Theorem: MyNat.mul_comm (MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

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

case succ
m n : MyNat
ih : m.mul n = n.mul m
⊢ m.mul n.succ = n.succ.mul m

State before:
case succ
m n : MyNat
ih : m.mul n = n.mul m
⊢ m.mul n.succ = n.succ.mul m
Tactic:
rw [mul, ih, succ_mul]
State after:
no goals

State before:
case zero
m : MyNat
⊢ m.mul zero = zero.mul m
Tactic:
rw [zero_mul]
State after:
case zero
m : MyNat
⊢ m.mul zero = zero

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