Finset.sum_range_id alternatives with Icc/Ico.. not range

Stream: Is there code for X?

[Safwane]

Hello everyone,
I'm a computational scientist and I'm fairly new to lean4. I only picked it up before graduating in 2023 for a few days then dropped it and now I'm attempting to actually sit down and learn it well. To do so I have decided to grind my way through the 1000 theorems list in hopes of getting comfortable enough with mathlib and lean to actually start contributing to the Numerical Analysis undergrad math section in mathlib :fingers_crossed:.
I'm starting with easy ones like Nicomachus Theorem and writing different proofs that use different concepts from mathlib and I was wondering if there's a way to have this:

example (n : ℕ) : ∑ i ∈ Finset.Icc 1 n, i = n * (n + 1) / 2 := by sorry

by leveraging a rewrite or a calc like below.

example (n: ℕ): ∑ i ∈ Finset.Icc 1 n, i = ∑ i ∈ Finset.range n+1, i := by sorry

I know I can just write a proof by induction which will be much easier but for the sake of me digging deeper into lean4 and mathlib I'm curious if there are other options. the more the better.

In other words, I'm asking about community approved practices when confronted with similar problems where a solution already exists in mathlib, like in this case sum_range_id exists for range but not for Intervals (as far as I know?)

Thanks Everyone.

[Kevin Buzzard]

do you really want to have pathological natural division in that statement? Your theorem is strictly weaker than what a mathematician would mean when they say $\sum_{i=1}^ni=n(n+1)/2$ because you are leaving open the possibility that the numerator is odd, i.e. you cannot deduce what a mathematician means by that claim from what you are formalizing, without further work (because $5/2=2$ in lean if the 5 is a natural). On the other hand this stronger statement

import Mathlib

example (n : ℕ) : ∑ i ∈ Finset.Icc 1 n, (i : ℚ) = n * (n + 1) / 2 := by sorry

(where the division now takes place in the rationals) is what a mathematician means by the assertion, and furthermore is easier to prove.

[Safwane]

TRUE. I still don't have coercion reflexes yet. thank you for pointing this out.
on a side note why does this

/-- Gauss' summation formula -/
theorem sum_range_id (n : ℕ) : ∑ i ∈ range n, i = n * (n - 1) / 2 := by
  rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ Nat.zero_lt_two]

from line 200 in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/BigOperators/Intervals.lean#L200
not have the type coerced? What am I missing?

[Kevin Buzzard]

It is true, it's just less helpful than you might think, for example you can't immediately deduce $2\sum_{i<n}i=n(n-1)$ from it.

[Kevin Buzzard]

Here's a proof by induction which reduces to the rational statement first.

import Mathlib

-- do we not have this?
lemma Nat.eq_div_of_cast_eq_div (a b c : ℕ) (h : (a : ℚ) = b / c) : a = b / c := by
  obtain rfl | hc := Nat.eq_zero_or_pos c
  · simp_all
  rw [eq_div_iff (by simp_all [hc.ne'])] at h
  norm_cast at h
  rw [← h, Nat.mul_div_cancel a hc]

example (n : ℕ) : ∑ i ∈ Finset.Icc 1 n, i = n * (n + 1) / 2 := by
  apply Nat.eq_div_of_cast_eq_div -- reduce to easier question about rationals
  push_cast
  induction n
  · simp
  · case succ d IH =>
    rw [Finset.sum_Icc_succ_top (by omega), IH]
    push_cast
    ring

You could probably use Finset.sum_Icc_succ_top and another lemma in the library about how natural division behaves ((a + 2b)/2 = a/2 + b etc) but it will be fiddlier; with this approach the only lemma you need is Finset.sum_Icc_succ_top and everything else can be done with tactics.