Theorem: MyNat.zero_add (IIScExperiments/NatAddMul.lean)

State before:
n : MyNat
⊢ 0 + n = n
Tactic:
induction' n with d hd
State after:
case zero

⊢ 0 + 0 = 0

case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d

State before:
case zero

⊢ 0 + 0 = 0

case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Tactic:
{ rfl }
State after:
case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d

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

State before:
case zero

⊢ 0 + 0 = 0
Tactic:
rfl
State after:
no goals

State before:
case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Tactic:
rw [add_succ]
State after:
case succ
d : MyNat
hd : 0 + d = d
⊢ succ (0 + d) = succ d

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