Imports
import Mathlib.TacticMiscellaneous
This page contains a proof of 2 \sum_{i=1}^{n} i = n (n + 1),
which you can look at to get a feel for formalized proofs in Lean.
Theorem: Cumulative Count
2 \sum_{i=1}^{n} i = n (n + 1)
Proof.
We can use induction to prove this result.
We can verify that for the base case of n = 1 we have that 2 ∑_{i = 1}^1 i = 2 · 1 = 2 = 1 (1 + 1).
The induction hypothesis is that 2 ∑_{i = 1}^k i = k (k + 1).
We verify the induction step by 2 ∑_{i = 1}^{k + 1} i = 2 ∑_{i = 1}^k i + 2 (k + 1) = k (k + 1) + 2 (k + 1) = 2 (k + 2) (k + 1) = 2 (k + 1) (k + 2).
■
example (n : Nat) :
2 * (∑ i ∈ Finset.range (n + 1), i) = n * (n + 1) := n:ℕ⊢ 2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1)
induction n with
⊢ 2 * ∑ i ∈ Finset.range (0 + 1), i = 0 * (0 + 1) All goals completed! 🐙
n:ℕih:2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1)⊢ 2 * ∑ i ∈ Finset.range (n + 1 + 1), i = (n + 1) * (n + 1 + 1)
n:ℕih:2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1)⊢ 2 * (∑ x ∈ Finset.range (n + 1), x + (n + 1)) = (n + 1) * (n + 1 + 1)
-- Expand the multiplication
n:ℕih:2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1)⊢ 2 * ∑ x ∈ Finset.range (n + 1), x + 2 * (n + 1) = (n + 1) * (n + 1 + 1)
-- Apply the induction hypothesis
n:ℕih:2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1)⊢ n * (n + 1) + 2 * (n + 1) = (n + 1) * (n + 1 + 1)
All goals completed! 🐙