Theorem: MyNat.add_assoc (MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
m n k : MyNat
⊢ (m.add n).add k = m.add (n.add k)
Tactic:
induction' k with k ih
State after:
case zero
m n : MyNat
⊢ (m.add n).add zero = m.add (n.add zero)

case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add n).add k.succ = m.add (n.add k.succ)

State before:
case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add n).add k.succ = m.add (n.add k.succ)
Tactic:
rw [add, ih]
State after:
case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add (n.add k)).succ = m.add (n.add k.succ)

State before:
case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add (n.add k)).succ = m.add (n.add k.succ)
Tactic:
rfl
State after:
no goals

State before:
case zero
m n : MyNat
⊢ (m.add n).add zero = m.add (n.add zero)
Tactic:
rfl
State after:
no goals