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

State before:
m n : MyNat
⊢ m + 1 + n = m + n + 1
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  dsimp
  congr 1
State after:
no goals

State before:
case zero
m : MyNat
⊢ m + 1 + zero = m + zero + 1
Tactic:
rfl
State after:
no goals

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

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