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

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

State before:
case zero
m : Nat
⊢ m + zero = zero + m
Tactic:
simp [zero_add, add_zero]
State after:
no goals

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