Theorem: sum_formula (Lectures/NatRec.lean)

State before:
n : ℕ
⊢ ↑(sumUpto n) = ↑n * (↑n + 1) / 2
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  simp [sumUpto, ih]
  linarith
State after:
no goals

State before:
case zero

⊢ ↑(sumUpto Nat.zero) = ↑Nat.zero * (↑Nat.zero + 1) / 2
Tactic:
rfl
State after:
no goals

State before:
case succ
n : ℕ
ih : ↑(sumUpto n) = ↑n * (↑n + 1) / 2
⊢ ↑(sumUpto (Nat.succ n)) = ↑(Nat.succ n) * (↑(Nat.succ n) + 1) / 2
Tactic:
simp [sumUpto, ih]
State after:
case succ
n : ℕ
ih : ↑(sumUpto n) = ↑n * (↑n + 1) / 2
⊢ ↑n + 1 + ↑n * (↑n + 1) / 2 = (↑n + 1) * (↑n + 1 + 1) / 2

State before:
case succ
n : ℕ
ih : ↑(sumUpto n) = ↑n * (↑n + 1) / 2
⊢ ↑n + 1 + ↑n * (↑n + 1) / 2 = (↑n + 1) * (↑n + 1 + 1) / 2
Tactic:
linarith
State after:
no goals