Lean4

aesop論理的な証明を自動探索するPlaintextexample (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by aesopexample (P Q : Prop) (hP : P) (hQ :...

linarith線形な等式・不等式から結論を導くPlaintextexample (x y : ℝ) (h₁ : x ≤ y) (h₂ : y ≤ x) : x = y := by linarithexample (x y : ℝ) (h₁...

ring可換環における多項式恒等式を証明するPlaintextexample (x y : ℤ) : (x + y)^2 = x^2 + 2*x*y + y^2 := by ringexample (x y : ℤ) : (x + y)^2...

norm_num数値計算を自動化するPlaintextexample : 2 + 3 = 5 := by norm_numexample : (7 : ℤ) ^ 2 = 49 := by norm_numexample : 2 + 3 = ...

congrArg等しいものに同じ関数を適用しても等しい、という事実を使うPlaintextexample (a b : α) (h : a = b) (f : α → β) : f a = f b := by exact congrArg ...

funext関数の等しさを、すべての入力での値の等しさに変えるPlaintextexample (f g : α → β) (h : ∀ x, f x = g x) : f = g := by funext x exact h x/-目標が...

ext関数や構造が等しいことを、各要素での等しさに帰着させるPlaintextexample (f g : α → β) (h : ∀ x, f x = g x) : f = g := by funext x exact h xexampl...

induction自然数や帰納的に定義された対象について帰納法を使うPlaintextexample (n : ℕ) : n + 0 = n := by induction n with | zero => rfl | succ n ih ...

by_cases命題が成り立つ場合と成り立たない場合に分けるPlaintextexample (P : Prop) [Decidable P] : P ∨ ¬P := by by_cases h : P · left exact h · r...

subst等式を使って変数を置き換えるPlaintextexample (a b : ℕ) (h : a = b) : a + a = b + b := by subst a rfl/-subst aにより、a = bを使って文脈中のaがb...