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

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

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

State before:
case zero
a : MyNat
⊢ a + 0 = 0 + a
Tactic:
rw [add_zero]
State after:
case zero
a : MyNat
⊢ a = 0 + a

State before:
case zero
a : MyNat
⊢ a = 0 + a
Tactic:
rw [zero_add]
State after:
no goals

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

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

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