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

State before:
a : MyNat
⊢ one * a = a
Tactic:
induction' a using MyNat.induction with d hd
State after:
case zero

⊢ one * 0 = 0

case succ
d : MyNat
hd : one * d = d
⊢ one * succ d = succ d

State before:
case zero

⊢ one * 0 = 0
Tactic:
rw [mul_zero]
State after:
no goals

State before:
case succ
d : MyNat
hd : one * d = d
⊢ one * succ d = succ d
Tactic:
rw [mul_succ, hd, one, add_succ, add_zero]
State after:
no goals