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

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

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

State before:
case succ
m n : MyNat
ih : m.succ.mul n = (m.mul n).add n
⊢ m.succ.mul n.succ = (m.mul n.succ).add n.succ
Tactic:
rw [mul, mul, ih, add_assoc, add_assoc, add_comm n, succ_add]
State after:
case succ
m n : MyNat
ih : m.succ.mul n = (m.mul n).add n
⊢ (m.mul n).add (m.add n).succ = (m.mul n).add (m.add n.succ)

State before:
case succ
m n : MyNat
ih : m.succ.mul n = (m.mul n).add n
⊢ (m.mul n).add (m.add n).succ = (m.mul n).add (m.add n.succ)
Tactic:
rfl
State after:
no goals

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