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

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

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

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

State before:
case zero
m : MyNat
⊢ add m zero = add zero m
Tactic:
rw [zero_add]
State after:
case zero
m : MyNat
⊢ add m zero = m

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