Theorem: sum_formula (GroupComp/NatRec.lean)

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

State before:
case zero

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

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

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