Telescoping alternating sums over ℤ with finsum in Lean/Mathlib

To show Σₙ (-1)ⁿ (cₙ + cₙ₊₁) = 0 for a finitely supported c : ℤ → M (Euler characteristic along a long exact sequence), use finsum with n.negOnePow • _ (ℤˣ smul). Rewrite n.negOnePow • c (n+1) = g (n+1) with g m := -(m.negOnePow • c m) (via Int.negOnePow_succ, Units.neg_smul, neg_neg), then finsum_comp_equiv (Equiv.addRight 1) (f := g) (exact works: Equiv.addRight 1 n is defeq n+1) and finsum_neg_distrib. Finiteness is now Function.HasFiniteSupport f (a def for f.support.Finite); for the shifted function use Set.Finite.preimage (Set.injOn_of_injective (add_left_injective 1)), and Function.support_fun_neg (not support_neg) for fun m => -f m. Set.finite_Icc on ℤ needs import Mathlib.Data.Int.Interval. Dependent-index gotcha: H^{n+1-1} is not syntactically H^n, so index the connecting-map image by its target degree, cₙ := [im δ_{n-1,n}], and prove independence of the source index by obtain rfl : m₁ = m₂ := by lia; rfl.