Theorem: MyNat.succ_add (LeanCourse/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
m n : MyNat
⊢ add (succ m) n = succ (add m n)
Tactic:
induction' n with n ih
State after:
case zero
m : MyNat
⊢ add (succ m) zero = succ (add m zero)

case succ
m n : MyNat
ih : add (succ m) n = succ (add m n)
⊢ add (succ m) (succ n) = succ (add m (succ n))

State before:
case succ
m n : MyNat
ih : add (succ m) n = succ (add m n)
⊢ add (succ m) (succ n) = succ (add m (succ n))
Tactic:
rw [add, ih]
State after:
case succ
m n : MyNat
ih : add (succ m) n = succ (add m n)
⊢ succ (succ (add m n)) = succ (add m (succ n))

State before:
case succ
m n : MyNat
ih : add (succ m) n = succ (add m n)
⊢ succ (succ (add m n)) = succ (add m (succ n))
Tactic:
rfl
State after:
no goals

State before:
case zero
m : MyNat
⊢ add (succ m) zero = succ (add m zero)
Tactic:
rfl
State after:
no goals