Theorem: nat_add_succ_is_succ_add (Katydid/Std/Lists.lean)

State before:
n m : ℕ
⊢ succ n + m = succ (n + m)
Tactic:
cases n with
| zero =>
  rewrite [Nat.add_comm]
  simp only [zero_eq, zero_add]
| succ n =>
  rewrite [Nat.add_comm]
  rewrite [Nat.add_comm (succ n)]
  repeat rewrite [Nat.add_succ]
  rfl
State after:
no goals

State before:
case zero
m : ℕ
⊢ succ zero + m = succ (zero + m)
Tactic:
rewrite [Nat.add_comm]
State after:
case zero
m : ℕ
⊢ m + succ zero = succ (zero + m)

State before:
case zero
m : ℕ
⊢ m + succ zero = succ (zero + m)
Tactic:
simp only [zero_eq, zero_add]
State after:
no goals

State before:
case succ
m n : ℕ
⊢ succ (succ n) + m = succ (succ n + m)
Tactic:
rewrite [Nat.add_comm]
State after:
case succ
m n : ℕ
⊢ m + succ (succ n) = succ (succ n + m)

State before:
case succ
m n : ℕ
⊢ m + succ (succ n) = succ (succ n + m)
Tactic:
rewrite [Nat.add_comm (succ n)]
State after:
case succ
m n : ℕ
⊢ m + succ (succ n) = succ (m + succ n)

State before:
case succ
m n : ℕ
⊢ m + succ (succ n) = succ (m + succ n)
Tactic:
repeat rewrite [Nat.add_succ]
State after:
case succ
m n : ℕ
⊢ succ (succ (m + n)) = succ (succ (m + n))

State before:
case succ
m n : ℕ
⊢ succ (succ (m + n)) = succ (succ (m + n))
Tactic:
rfl
State after:
no goals

State before:
case succ
m n : ℕ
⊢ succ (m + (n + 1)) = succ (m + succ n)
Tactic:
rewrite [Nat.add_succ]
State after:
case succ
m n : ℕ
⊢ succ (succ (m + n)) = succ (succ (m + n))