Mathlib Finset sum reindexing: which lemma to reach for (v4.35)
All compiled on Mathlib v4.35.0. (1) Shift or any explicit bijection with an explicit inverse: Finset.sum_nbij' i j takes plain functions (no membership proofs), and all five side goals are membership/inverse facts. apply Finset.sum_nbij' (· + 1) (· - 1) <;> simp <;> omega proves ∑ i ∈ range n, f (i + 1) = ∑ i ∈ Icc 1 n, f i. sum_bij'/sum_bij take maps (a : ι) → a ∈ s → κ and are only worth it when the map needs the membership proof. sum_nbij i wants Set.InjOn and Set.SurjOn instead of an inverse. sum_equiv e and sum_bijective e are for global bijections, with the side condition i ∈ s ↔ e i ∈ t. (2) Interval shifts without bijections: rw [← Finset.Ico_add_one_right_eq_Icc, Finset.sum_Ico_eq_sum_range]; simp [add_comm] (Nat.Ico_succ_right no longer exists). (3) Ready-made: sum_range_reflect f n (f (n-1-j)), Fin.sum_univ_eq_sum_range f n, sum_map s e f for an embedding such as addRightEmbedding 1, and sum_image (needs Set.InjOn g s; for negation on ℤ, by simp [Set.InjOn] discharges it).
Confirmed on Lean/Mathlib v4.35.0. Both proofs in (1) and (2) compile as written, all the lemmas in (3) have the stated shapes, the
sum_imagenegation example closes withby simp [Set.InjOn], andNat.Ico_succ_rightis an unknown constant. One precision on (1): ofsum_nbij''s five hypotheses, four are membership/inverse facts (i a ∈ t, j a ∈ s, j (i a) = a, i (j a) = a). The fifth is the summand equation∀ a ∈ s, f a = g (i a), which in the example happens to be closed by simp. In general that is the goal that needs real work. Likewisesum_equivandsum_bijectivetake that summand hypothesis in addition toi ∈ s ↔ e i ∈ t.