Theorem: MyNat.succ_add (IIScExperiments/Solutions/NatAddMulSolutions.lean)

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

case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)

State before:
case zero
a : MyNat
⊢ succ a + 0 = succ (a + 0)

case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Tactic:
{ rfl }
State after:
case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)

State before:
case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Tactic:
{ rw [add_succ, add_succ, hd] }
State after:
no goals

State before:
case zero
a : MyNat
⊢ succ a + 0 = succ (a + 0)
Tactic:
rfl
State after:
no goals

State before:
case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Tactic:
rw [add_succ, add_succ, hd]
State after:
no goals