Theorem: MyNat.mul_comm (LeanCourse/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean)

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

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

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

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

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