internlm/Lean-Github huggingface dataset:
Theorem: Imo1964P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
have h12 : 0 ≤ (c - a) * (c - b) := by nlinarith only [Hba, Hcb]
Proof state after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Theorem: Imo1964P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
have h13 : 0 ≤ c * (c - a) * (c - b) := by nlinarith only [hc, h12]
Proof state after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
h13 : 0 ≤ c * (c - a) * (c - b)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Theorem: Imo1964P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
h13 : 0 ≤ c * (c - a) * (c - b)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1964P2.schur
Proof state before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hcb : ¬c ≤ b
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
have h3 : b ≤ c := le_of_not_le Hcb
Proof state after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Theorem: Imo1964P2.schur
Proof state before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
linarith [h1 ha hc hb h3]
Proof state after:
no goals
Theorem: Imo1964P2.schur
Proof state before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
have h4 : a ≤ b := le_of_not_le Hba
Proof state after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Theorem: Imo1964P2.schur
Proof state before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
obtain hca | hac : c ≤ a ∨ a ≤ c := le_total c a
Proof state after:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Theorem: Imo1964P2.schur
Proof state before:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
have := h2 hb ha hc hca h4
Proof state after:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : 0 ≤ b * (b - a) * (b - c) + a * (a - b) * (a - c) + c * (c - b) * (c - a)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Theorem: Imo1964P2.schur
Proof state before:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : 0 ≤ b * (b - a) * (b - c) + a * (a - b) * (a - c) + c * (c - b) * (c - a)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
linarith only [this]
Proof state after:
no goals
Theorem: Imo1964P2.schur
Proof state before:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
have := h2 hb hc ha hac Hcb
Proof state after:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
this : 0 ≤ b * (b - c) * (b - a) + c * (c - b) * (c - a) + a * (a - b) * (a - c)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Theorem: Imo1964P2.schur
Proof state before:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ {a b c : ℝ},
    0 ≤ a → 0 ≤ b → 0 ≤ c → c ≤ b → b ≤ a → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
this : 0 ≤ b * (b - c) * (b - a) + c * (c - b) * (c - a) + a * (a - b) * (a - c)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
linarith only [this]
Proof state after:
no goals
Theorem: Imo1964P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
⊢ a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1964P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ (a - b) * (a * (a - c) - b * (b - c))
Tactic:
apply mul_nonneg
Proof state after:
case ha
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a - b

case hb
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a * (a - c) - b * (b - c)
Theorem: Imo1964P2.schur
Proof state before:
case ha
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a - b
Tactic:
exact sub_nonneg_of_le Hba
Proof state after:
no goals
Theorem: Imo1964P2.schur
Proof state before:
case hb
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a * (a - c) - b * (b - c)
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Imo1964P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ 0 ≤ (c - a) * (c - b)
Tactic:
nlinarith only [Hba, Hcb]
Proof state after:
no goals
Theorem: Imo1964P2.schur
Proof state before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ 0 ≤ c * (c - a) * (c - b)
Tactic:
nlinarith only [hc, h12]
Proof state after:
no goals
Theorem: Iran1998P3.cube_root_cube
Proof state before:
x : ℝ
h : 0 ≤ x
⊢ (x ^ 3) ^ (1 / 3) = x
Tactic:
rw [←Real.rpow_mul h, mul_div_cancel₀ (1 : ℝ) three_ne_zero]
Proof state after:
x : ℝ
h : 0 ≤ x
⊢ x ^ 1 = x
Theorem: Iran1998P3.cube_root_cube
Proof state before:
x : ℝ
h : 0 ≤ x
⊢ x ^ 1 = x
Tactic:
exact Real.rpow_one x
Proof state after:
no goals
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
p : Prop
⊢ p ∨ ¬p
Tactic:
suffices ¬¬ (p ∨ ¬ p) by
  apply assumed_dne; assumption
Proof state after:
p : Prop
⊢ ¬¬(p ∨ ¬p)
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
p : Prop
⊢ ¬¬(p ∨ ¬p)
Tactic:
intro
Proof state after:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ False
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ False
Tactic:
have h : ¬ p ∧ ¬¬p := by
  rw [← de_morgan_1]  assumption
Proof state after:
p : Prop
a✝ : ¬(p ∨ ¬p)
h : ¬p ∧ ¬¬p
⊢ False
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
p : Prop
a✝ : ¬(p ∨ ¬p)
h : ¬p ∧ ¬¬p
⊢ False
Tactic:
cases h with
| intro hnp hnnp => contradiction
Proof state after:
no goals
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
p : Prop
this : ¬¬(p ∨ ¬p)
⊢ p ∨ ¬p
Tactic:
apply assumed_dne
Proof state after:
case h
p : Prop
this : ¬¬(p ∨ ¬p)
⊢ ¬¬(p ∨ ¬p)
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
case h
p : Prop
this : ¬¬(p ∨ ¬p)
⊢ ¬¬(p ∨ ¬p)
Tactic:
assumption
Proof state after:
no goals
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ ¬p ∧ ¬¬p
Tactic:
rw [← de_morgan_1]
Proof state after:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ ¬(p ∨ ¬p)
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ ¬(p ∨ ¬p)
Tactic:
assumption
Proof state after:
no goals
Theorem: alt_classical_redux.alt_classical_redux_em
Proof state before:
case intro
p : Prop
a✝ : ¬(p ∨ ¬p)
hnp : ¬p
hnnp : ¬¬p
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: PartialComposition.comp_all_none_with
Proof state before:
α β γ : Type
g : α → Option β
x : α
⊢ comp_partial all_none g x = Option.none
Tactic:
simp [comp_partial, all_none]
Proof state after:
α β γ : Type
g : α → Option β
x : α
⊢ (match g x with
    | Option.none => Option.none
    | Option.some y => Option.none) =
    Option.none
Theorem: PartialComposition.comp_all_none_with
Proof state before:
α β γ : Type
g : α → Option β
x : α
⊢ (match g x with
    | Option.none => Option.none
    | Option.some y => Option.none) =
    Option.none
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: PartialComposition.comp_with_all_none
Proof state before:
α β γ : Type
f : β → Option γ
x : α
⊢ comp_partial f all_none x = Option.none
Tactic:
simp [comp_partial, all_none]
Proof state after:
no goals
Theorem: PartialComposition.comp_all_none_with_eq_all_none
Proof state before:
α β γ : Type
g : α → Option β
x✝ : α
⊢ comp_partial all_none g = all_none
Tactic:
funext
Proof state after:
case h
α β γ : Type
g : α → Option β
x✝¹ x✝ : α
⊢ comp_partial all_none g x✝ = all_none x✝
Theorem: PartialComposition.comp_all_none_with_eq_all_none
Proof state before:
case h
α β γ : Type
g : α → Option β
x✝¹ x✝ : α
⊢ comp_partial all_none g x✝ = all_none x✝
Tactic:
apply comp_all_none_with
Proof state after:
no goals
Theorem: PartialComposition.comp_with_all_none_eq_all_none
Proof state before:
α β γ : Type
f : β → Option γ
x✝ : α
⊢ comp_partial f all_none = all_none
Tactic:
funext
Proof state after:
case h
α β γ : Type
f : β → Option γ
x✝¹ x✝ : α
⊢ comp_partial f all_none x✝ = all_none x✝
Theorem: PartialComposition.comp_with_all_none_eq_all_none
Proof state before:
case h
α β γ : Type
f : β → Option γ
x✝¹ x✝ : α
⊢ comp_partial f all_none x✝ = all_none x✝
Tactic:
apply comp_with_all_none
Proof state after:
no goals
Theorem: MyNat.add_zero
Proof state before:
m : Nat
⊢ m + zero = m
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_succ
Proof state before:
m k : Nat
⊢ m + succ k = succ (m + k)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
m : Nat
⊢ zero + m = m
Tactic:
induction m with
| zero => rfl
| succ k ih =>
  rw [add_succ, ih]
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case zero

⊢ zero + zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case succ
k : Nat
ih : zero + k = k
⊢ zero + succ k = succ k
Tactic:
rw [add_succ, ih]
Proof state after:
no goals
Theorem: MyNat.zero_add_by_rec
Proof state before:
m : Nat
⊢ zero + zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_add_by_rec
Proof state before:
m a : Nat
ih : zero + a = a
⊢ zero + succ a = succ a
Tactic:
rw [add_succ, ih]
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
m n k : Nat
⊢ m + n + k = m + (n + k)
Tactic:
induction k with
| zero => repeat (apply add_zero)
| succ l ih =>
  repeat (rw [add_succ])
  rw [ih]
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case zero
m n : Nat
⊢ m + n + zero = m + (n + zero)
Tactic:
repeat (apply add_zero)
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case zero
m n : Nat
⊢ m + n + zero = m + (n + zero)
Tactic:
(apply add_zero)
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case zero
m n : Nat
⊢ m + n + zero = m + (n + zero)
Tactic:
apply add_zero
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ m + n + succ l = m + (n + succ l)
Tactic:
repeat (rw [add_succ])
Proof state after:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = succ (m + (n + l))
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = succ (m + (n + l))
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = m + succ (n + l)
Tactic:
(rw [add_succ])
Proof state after:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = succ (m + (n + l))
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = m + succ (n + l)
Tactic:
rw [add_succ]
Proof state after:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = succ (m + (n + l))
Theorem: MyNat.succ_add
Proof state before:
m k : Nat
⊢ succ k + m = succ (k + m)
Tactic:
induction m with
| zero => rfl
| succ l ih =>
  rw [add_succ, add_succ, ih]
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
case zero
k : Nat
⊢ succ k + zero = succ (k + zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
case succ
k l : Nat
ih : succ k + l = succ (k + l)
⊢ succ k + succ l = succ (k + succ l)
Tactic:
rw [add_succ, add_succ, ih]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
m n : Nat
⊢ m + n = n + m
Tactic:
induction n with
| zero => simp [zero_add, add_zero]
| succ l ih => simp [succ_add, add_succ, ih]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
case zero
m : Nat
⊢ m + zero = zero + m
Tactic:
simp [zero_add, add_zero]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
case succ
m l : Nat
ih : m + l = l + m
⊢ m + succ l = succ l + m
Tactic:
simp [succ_add, add_succ, ih]
Proof state after:
no goals
Theorem: MyNat.one_eq_succ_zero
Proof state before:
⊢ one = succ zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.lit_one_eq_succ_zero
Proof state before:
⊢ 1 = succ zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.lit_zero_eq_zero
Proof state before:
⊢ 0 = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_eq_add_one
Proof state before:
n : Nat
⊢ succ n = n + one
Tactic:
rw [one_eq_succ_zero, add_succ, add_zero]
Proof state after:
no goals
Theorem: MyNat.add_comm_right
Proof state before:
a b c : Nat
⊢ a + b + c = a + (b + c)
Tactic:
rw [add_assoc]
Proof state after:
no goals
Theorem: MyNat.add_comm_right
Proof state before:
a b c : Nat
⊢ a + (b + c) = a + (c + b)
Tactic:
rw [add_comm b c]
Proof state after:
no goals
Theorem: MyNat.add_comm_right
Proof state before:
a b c : Nat
⊢ a + (c + b) = a + c + b
Tactic:
rw [add_assoc]
Proof state after:
no goals
Theorem: MyNat.add_left_comm
Proof state before:
a b c : Nat
⊢ a + (b + c) = b + (a + c)
Tactic:
rw [← add_assoc, add_comm a b, add_assoc]
Proof state after:
no goals
Theorem: MyNat.succ_pred
Proof state before:
n : Nat
⊢ n ≠ zero → succ (pred n) = n
Tactic:
intro h
Proof state after:
n : Nat
h : n ≠ zero
⊢ succ (pred n) = n
Theorem: MyNat.succ_pred
Proof state before:
n : Nat
h : n ≠ zero
⊢ succ (pred n) = n
Tactic:
simp [pred]
Proof state after:
n : Nat
h : n ≠ zero
⊢ succ
      (match n with
      | zero => zero
      | succ k => k) =
    n
Theorem: MyNat.succ_pred
Proof state before:
n : Nat
h : n ≠ zero
⊢ succ
      (match n with
      | zero => zero
      | succ k => k) =
    n
Tactic:
split
Proof state after:
case h_1
x✝ : Nat
h : zero ≠ zero
⊢ succ zero = zero

case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝
Theorem: MyNat.succ_pred
Proof state before:
case h_1
x✝ : Nat
h : zero ≠ zero
⊢ succ zero = zero

case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝
Tactic:
. contradiction
Proof state after:
case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝
Theorem: MyNat.succ_pred
Proof state before:
case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝
Tactic:
. rfl
Proof state after:
no goals
Theorem: MyNat.succ_pred
Proof state before:
case h_1
x✝ : Nat
h : zero ≠ zero
⊢ succ zero = zero
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.succ_pred
Proof state before:
case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.pred_succ
Proof state before:
n : Nat
⊢ pred (succ n) = n
Tactic:
simp [pred]
Proof state after:
no goals
Theorem: MyNat.add_pred
Proof state before:
m n : Nat
⊢ n ≠ zero → m + pred n = pred (m + n)
Tactic:
intro
Proof state after:
m n : Nat
a✝ : n ≠ zero
⊢ m + pred n = pred (m + n)
Theorem: MyNat.add_pred
Proof state before:
m n : Nat
a✝ : n ≠ zero
⊢ m + pred n = pred (m + n)
Tactic:
match n with
| zero => contradiction
| succ l =>
  rw [add_succ, pred_succ, pred_succ]
Proof state after:
no goals
Theorem: MyNat.add_pred
Proof state before:
m n : Nat
a✝ : zero ≠ zero
⊢ m + pred zero = pred (m + zero)
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.add_pred
Proof state before:
m n l : Nat
a✝ : succ l ≠ zero
⊢ m + pred (succ l) = pred (m + succ l)
Tactic:
rw [add_succ, pred_succ, pred_succ]
Proof state after:
no goals
Theorem: MyNat.pred_add
Proof state before:
m n : Nat
⊢ m ≠ zero → pred m + n = pred (m + n)
Tactic:
intro hm
Proof state after:
m n : Nat
hm : m ≠ zero
⊢ pred m + n = pred (m + n)
Theorem: MyNat.pred_add
Proof state before:
m n : Nat
hm : m ≠ zero
⊢ pred m + n = pred (m + n)
Tactic:
rw [add_comm (pred m) n, add_pred n m hm, add_comm]
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
a : Nat
⊢ zero * a = zero
Tactic:
induction a
Proof state after:
case zero

⊢ zero * zero = zero

case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero
Theorem: MyNat.zero_mul
Proof state before:
case zero

⊢ zero * zero = zero

case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero
Tactic:
. rfl
Proof state after:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero
Theorem: MyNat.zero_mul
Proof state before:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero
Tactic:
. rw [mul_succ, add_zero]
  assumption
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
case zero

⊢ zero * zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero
Tactic:
rw [mul_succ, add_zero]
Proof state after:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * a✝ = zero
Theorem: MyNat.zero_mul
Proof state before:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * a✝ = zero
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.mul_one
Proof state before:
a : Nat
⊢ a * one = a
Tactic:
rw [one_eq_succ_zero, mul_succ, mul_zero, zero_add]
Proof state after:
no goals
Theorem: MyNat.one_mul
Proof state before:
a : Nat
⊢ one * a = a
Tactic:
induction a with
| zero => rw [mul_zero]
| succ a' ih => rw [mul_succ, ih, succ_eq_add_one]
Proof state after:
no goals
Theorem: MyNat.one_mul
Proof state before:
case zero

⊢ one * zero = zero
Tactic:
rw [mul_zero]
Proof state after:
no goals
Theorem: MyNat.one_mul
Proof state before:
case succ
a' : Nat
ih : one * a' = a'
⊢ one * succ a' = succ a'
Tactic:
rw [mul_succ, ih, succ_eq_add_one]
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
t a b : Nat
⊢ t * (a + b) = t * a + t * b
Tactic:
induction b with
| zero =>
  rw [add_zero, mul_zero, add_zero]
| succ b' ih =>
  rw [add_succ, mul_succ, ih, mul_succ, add_assoc]
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
case zero
t a : Nat
⊢ t * (a + zero) = t * a + t * zero
Tactic:
rw [add_zero, mul_zero, add_zero]
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
case succ
t a b' : Nat
ih : t * (a + b') = t * a + t * b'
⊢ t * (a + succ b') = t * a + t * succ b'
Tactic:
rw [add_succ, mul_succ, ih, mul_succ, add_assoc]
Proof state after:
no goals
Theorem: MyNat.mul_assoc
Proof state before:
a b c : Nat
⊢ a * b * c = a * (b * c)
Tactic:
induction c with
| zero => repeat (rw [mul_zero])
| succ c' ih =>
  repeat (rw [mul_succ])
  rw [mul_add]
  rw [ih]
Proof state after:
no goals
Theorem: MyNat.mul_assoc
Proof state before:
case zero
a b : Nat
⊢ a * b * zero = a * (b * zero)
Tactic:
repeat (rw [mul_zero])
Proof state after:
no goals
Theorem: MyNat.mul_assoc
Proof state before:
case zero
a b : Nat
⊢ zero = a * zero
Tactic:
(rw [mul_zero])
Proof state after:
no goals
Theorem: MyNat.mul_assoc
Proof state before:
case zero
a b : Nat
⊢ zero = a * zero
Tactic:
rw [mul_zero]
Proof state after:
no goals
Theorem: MyNat.mul_assoc
Proof state before:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * succ c' = a * (b * succ c')
Tactic:
repeat (rw [mul_succ])
Proof state after:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * c' + b)