Theorem: sum_formula (PnP2023/Extras/SumToN.lean)

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

State before:
case zero

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

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

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

State before:
case succ
n : ℕ
ih : 2 * sumTo n = n * (n + 1)
⊢ 2 * n + 2 + (n * n + n) = Nat.succ n * Nat.succ n + Nat.succ n
Tactic:
linarith
State after:
no goals