Theorem: MyNat.succ_mul (IIScExperiments/Solutions/NatAddMulExperiments.lean)

State before:
a b : MyNat
⊢ succ a * b = a * b + b
Tactic:
induction' b using MyNat.induction with d hd
State after:
case zero
a : MyNat
⊢ succ a * 0 = a * 0 + 0

case succ
a d : MyNat
hd : succ a * d = a * d + d
⊢ succ a * succ d = a * succ d + succ d

State before:
case zero
a : MyNat
⊢ succ a * 0 = a * 0 + 0
Tactic:
rw [mul_zero, mul_zero, add_zero]
State after:
no goals

State before:
case succ
a d : MyNat
hd : succ a * d = a * d + d
⊢ succ a * succ d = a * succ d + succ d
Tactic:
rw [mul_succ, hd, mul_succ, succ_eq_add_one, succ_eq_add_one, add_add_add]
State after:
no goals