Reindexing index-0 sum to index-1 sum

Stream: new members

[Li Xuanji]

Is there a way to improve this proof?

import Mathlib

theorem ri
(i : ℕ)
(a : ℕ → ℝ)
: ∑ x ∈ Finset.range i, a (x + 1) = ∑ x ∈ Finset.Ico 1 (i + 1), a x := by
  apply Finset.sum_bij (fun x _ ↦ x + 1)
  simp
  simp
  simp
  intro b h1 h2
  use b-1
  constructor
  omega
  omega
  intro t1 t2
  rfl

I would in particular be interested if there's a way to prove this without 4 subgoals

(For the reader's convenience, this is the theorem statement in LaTeX)

image.png

[Matt Diamond]

I think docs#Finset.sum_image may help

[Matt Diamond]

import Mathlib

theorem ri
(i : ℕ)
(a : ℕ → ℝ)
: ∑ x ∈ Finset.range i, a (x + 1) = ∑ x ∈ Finset.Ico 1 (i + 1), a x := by
  have : Finset.Ico 1 (i + 1) = Finset.image (· + 1) (Finset.range i) :=
    by rw [Finset.range_eq_Ico, Finset.image_add_right_Ico]
  rw [this, Finset.sum_image (by simp)]

[Matt Diamond]

I wouldn't be surprised if there was a direct proof somewhere in this file:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Intervals.html

a lot of Finset.sum interval offset lemmas...

[Matt Diamond]

ah, yes, there's a one-liner:

import Mathlib

theorem ri
(i : ℕ)
(a : ℕ → ℝ)
: ∑ x ∈ Finset.range i, a (x + 1) = ∑ x ∈ Finset.Ico 1 (i + 1), a x := by
  rw [Finset.range_eq_Ico, Finset.sum_Ico_add']