Theorem: MyNat.add_comm (Talk/06Induction.lean)

State before:
m n : MyNat
⊢ m + n = n + m
Tactic:
induction n with
| zero =>
  dsimp
  rw [zero_add]
| succ n ih =>
  dsimp
  rw [one_add_add]
  rw [ih]
State after:
no goals

State before:
case zero
m : MyNat
⊢ m + zero = zero + m
Tactic:
dsimp
State after:
case zero
m : MyNat
⊢ m = 0 + m

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

State before:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + succ n = succ n + m
Tactic:
dsimp
State after:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + n + 1 = n + 1 + m

State before:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + n + 1 = n + 1 + m
Tactic:
rw [one_add_add]
State after:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + n + 1 = n + m + 1

State before:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + n + 1 = n + m + 1
Tactic:
rw [ih]
State after:
no goals