2026-07

change現在の目標を、定義上等しい別の目標へ変更するPlaintextexample : myFrobeniusFun K p 1 = 1 := by change 1 ^ p = 1 exact one_pow pexample : ...

show現在の目標を、定義上同じ別の形で表示し直すPlaintextexample (n : ℕ) : n + 0 = n := by show n + 0 = n exact Nat.add_zero nexample (n : ℕ) :...

have証明の途中で補助的な事実を作るPlaintextexample (a b c : ℕ) (h₁ : a = b) (h₂ : b = c) : a = c := by have h₃ : a = c := by exact Eq.t...

use存在命題の証人を指定するPlaintextexample : ∃ n : ℕ, n = 3 := by use 3example : ∃ n : ℕ, n = 3 := by use 3

refine証明の一部を与え、残りを穴?_として新しい目標にするPlaintextexample (P : ℕ → Prop) (n : ℕ) (h : P n) : ∃ m, P m := by refine ⟨n, ?_⟩ exact ...

rcases存在命題、連言、部分型などを分解するときに使うPlaintextexample (P : ℕ → Prop) (h : ∃ n, P n) : ∃ n, P n := by rcases h with ⟨n, hn⟩ exact...

cases仮定を場合分けしたり、構造を分解したりするPlaintextexample (P Q : Prop) (h : P ∨ Q) : Q ∨ P := by cases h with | inl hP => right exact h...

left,right目標が「または」のとき、どちらを証明するか選ぶPlaintextexample (P Q : Prop) (hP : P) : P ∨ Q := by left exact hP example (P Q : Prop)...

constructor目標が「かつ」や、複数の欄を持つ構造の場合に、目標を分割するPlaintextexample (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by constructor · exa...

simpasimpで式を簡約したあと、与えた証明を使うPlaintextexample (n : ℕ) : n + 0 = n := by simpa using Nat.add_zero nexample (n : ℕ) : n + 0 ...