Lean4

simp定義や基本的な等式を使って、式を自動的に簡単にするPlaintextexample (n : ℕ) : n + 0 = n := by simpexample (n : ℕ) : n + 0 = n := by simp定義を指定し...

rw等式を使って書き換えるPlaintextexample (a b c : ℕ) (h : a = b) : a + c = b + c := by rw [h]example (a b c : ℕ) (h : a = b) : a + ...

unfold定義を展開するPlaintextdef double (n : ℕ) : ℕ := n + nexample (n : ℕ) : double n = n + n := by unfold doubledef double (n...

apply目標を証明するために使えそうな定理を適用し、残りの条件を新しい目標にするPlaintextexample (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := by apply hPQ exact ...

intro「任意の〜について」や「〜ならば」を証明するときに、変数や仮定を導入する全称命題の例Plaintextexample : ∀ n : ℕ, n = n := by intro n rfl /-最初の目標は、⊢ ∀ n : ℕ, n...

rfl左右が定義上同じであることを示すPlaintextexample (x : ℕ) : x = x := by rfl/-x（左辺）とx（右辺）は同じ-/example (x : ℕ) : x = x := by rfl/-x（左辺）と...

exact目標と全く同じ型の証明を与えるPlaintextexample (P : Prop) (h : P) : P := by exact h /-hがまさに目標Pの証明なので、「exact h」で終了する-/example (P : ...

#check#checkで型をチェックできる

theoremtheoremを使って定理をかける