Theorem: MyNat.add_assoc (LeanCourse/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean)

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

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

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

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

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