Theorem: MyNat.add_assoc (TheoremProvingLean/inductive_types.lean)

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]
State after:
no goals

State before:
case zero
m n : Nat
⊢ m + n + zero = m + (n + zero)
Tactic:
repeat (apply add_zero)
State after:
no goals

State before:
case zero
m n : Nat
⊢ m + n + zero = m + (n + zero)
Tactic:
(apply add_zero)
State after:
no goals

State before:
case zero
m n : Nat
⊢ m + n + zero = m + (n + zero)
Tactic:
apply add_zero
State after:
no goals

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])
State after:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = succ (m + (n + l))

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]
State after:
no goals

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])
State after:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = succ (m + (n + l))

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]
State after:
case succ
m n l : Nat
ih : m + n + l = m + (n + l)
⊢ succ (m + n + l) = succ (m + (n + l))