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

State before:
a b : Nat
⊢ a * b = b * a
Tactic:
induction b with
| zero => simp
| succ b' ih => rw [mul_succ, succ_mul, ih]
State after:
no goals

State before:
case zero
a : Nat
⊢ a * zero = zero * a
Tactic:
simp
State after:
no goals

State before:
case succ
a b' : Nat
ih : a * b' = b' * a
⊢ a * succ b' = succ b' * a
Tactic:
rw [mul_succ, succ_mul, ih]
State after:
no goals