Dealing with indices in summations over finsets

Stream: mathlib4

[Javier Burroni]

I’m trying to write a proof that involves dealing with summations (I described the idea in this post: https://proofassistants.stackexchange.com/q/4393/5231).

At some point in the proof, I have to perform some telescoping summations to cancel certain terms.
However, I am stuck when trying to expand the summation.

I reduced the code to the following piece:

instance (α : Type) [Fintype α] : Coe (Fin (Fintype.card α - 1)) (Fin (Fintype.card α)) where
  coe a := Fin.mk a.val (by
    have h : a.val < Fintype.card α - 1 := a.isLt
    exact Nat.lt_of_lt_pred h)

def finSucc {α : Type} [Fintype α]
    (i : Fin (Fintype.card α - 1)) : Fin (Fintype.card α) :=
  ⟨i.succ, by exact Nat.add_lt_of_lt_sub i.is_lt⟩

/-NeZero is required for the casting to work -/
theorem sum_finSucc_eq {α : Type} [Fintype α] [NeZero (Fintype.card α)]
    (r : Fin (Fintype.card α) → ℚ) (h_gt : 1 < Fintype.card α)
    : ∑ i : Fin (Fintype.card α - 1), r (finSucc i)
    = r ↑(Fintype.card α - 1) + (∑ i : Fin (Fintype.card α - 1), r i)
    - r (0 : Fin (Fintype.card α)) := by
  sorry

I would appreciate any help with this.

[Ruben Van de Velde]

Do you need to use Fin? Things might be easier indexing with plain naturals. Even if that's not an option, maybe it's helpful to try to finish the proof in that setting first and then see if you can translate to Fin

[Javier Burroni]

Hi,
Yes, the Fin is necessary in the question for two reasons:

1. I'm using an orderIsoOfFin to do a summation in an ordered way. Hence, the first and last elements carry a particular meaning, and
2. the Fin type is what makes this a question worth asking in here.