Theorem: Nat.add_pred (Algdata/Init/Nat.lean)

State before:
m n : Nat
⊢ n > 0 → m + pred n = pred (m + n)
Tactic:
intro hn
State after:
m n : Nat
hn : n > 0
⊢ m + pred n = pred (m + n)

State before:
m n : Nat
hn : n > 0
⊢ m + pred n = pred (m + n)
Tactic:
cases n
State after:
case zero
m : Nat
hn : zero > 0
⊢ m + pred zero = pred (m + zero)

case succ
m n✝ : Nat
hn : succ n✝ > 0
⊢ m + pred (succ n✝) = pred (m + succ n✝)

State before:
m : Nat
hn : zero > 0
⊢ m + pred zero = pred (m + zero)
Tactic:
case zero =>
  exact (zero.not_lt_zero hn).elim
State after:
no goals

State before:
m n : Nat
hn : succ n > 0
⊢ m + pred (succ n) = pred (m + succ n)
Tactic:
case succ n =>
  simp [Nat.add_succ]
State after:
no goals

State before:
m : Nat
hn : zero > 0
⊢ m + pred zero = pred (m + zero)
Tactic:
exact (zero.not_lt_zero hn).elim
State after:
no goals

State before:
m n : Nat
hn : succ n > 0
⊢ m + pred (succ n) = pred (m + succ n)
Tactic:
simp [Nat.add_succ]
State after:
no goals