Theorem: sum_id (LeanCourse/Lectures/Lecture7Before.lean)

State before:
n✝ n : ℕ
⊢ ∑ i in Finset.range (n + 1), i = n * (n + 1) / 2
Tactic:
sorry
State after:
no goals