feat: Better lemmas for transferring finite sums along equivalences (#9237)

Lemmas around this were a mess, throth in terms of names, statement and location. This PR standardises everything to be in `Algebra.BigOperators.Basic` and changes the lemmas to take in `InjOn` and `SurjOn` assumptions where possible (and where impossible make sure the hypotheses are taken in the correct order) and moves the equality of functions hypothesis last.

Also add a few lemmas that help fix downstream uses by golfing.

From LeanAPAP and LeanCamCombi

Author: YaelDillies

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1240,14 +1240,10 @@ theorem finprod_mem_finset_product' [DecidableEq α] [DecidableEq β] (s : Finse
     (f : α × β → M) :
     (∏ᶠ (ab) (_ : ab ∈ s), f ab) =
       ∏ᶠ (a) (b) (_ : b ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd), f (a, b) := by
-  have :
-    ∀ a,
-      (∏ i : β in (s.filter fun ab => Prod.fst ab = a).image Prod.snd, f (a, i)) =
-        (Finset.filter (fun ab => Prod.fst ab = a) s).prod f := by
-    refine' fun a => Finset.prod_bij (fun b _ => (a, b)) _ _ _ _ <;> simp
-    suffices ∀ a' b, (a', b) ∈ s → a' = a → (a, b) ∈ s ∧ a' = a by simpa
-    rintro a' b hp rfl
-    exact ⟨hp, rfl⟩
+  have (a) :
+      ∏ i in (s.filter fun ab => Prod.fst ab = a).image Prod.snd, f (a, i) =
+        (s.filter (Prod.fst · = a)).prod f := by
+    refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_ <;> aesop
   rw [finprod_mem_finset_eq_prod]
   simp_rw [finprod_mem_finset_eq_prod, this]
   rw [finprod_eq_prod_of_mulSupport_subset _

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -645,7 +645,7 @@ lemma indicator_eq_sum_attach_single [AddCommMonoid M] {s : Finset α} (f : ∀
 
 lemma indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : α → M) :
     indicator s (fun x _ ↦ f x) = ∑ x in s, single x (f x) :=
-  (indicator_eq_sum_attach_single _).trans <| sum_attach (f := fun x ↦ single x (f x))
+  (indicator_eq_sum_attach_single _).trans <| sum_attach _ fun x ↦ single x (f x)
 
 @[to_additive (attr := simp)]
 lemma prod_indicator_index_eq_prod_attach [Zero M] [CommMonoid N]
@@ -661,7 +661,7 @@ lemma prod_indicator_index_eq_prod_attach [Zero M] [CommMonoid N]
 lemma prod_indicator_index [Zero M] [CommMonoid N]
     {s : Finset α} (f : α → M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) :
     (indicator s (fun x _ ↦ f x)).prod h = ∏ x in s, h x (f x) :=
-  (prod_indicator_index_eq_prod_attach _ h_zero).trans <| prod_attach (f := fun x ↦ h x (f x))
+  (prod_indicator_index_eq_prod_attach _ h_zero).trans <| prod_attach _ fun x ↦ h x (f x)
 
 lemma sum_cons [AddCommMonoid M] (n : ℕ) (σ : Fin n →₀ M) (i : M) :
     (sum (cons i σ) fun _ e ↦ e) = i + sum σ (fun _ e ↦ e) := by

Mathlib/Algebra/BigOperators/Finsupp.lean

@@ -123,10 +123,8 @@ theorem sum_Ico_Ico_comm {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ →
     (∑ i in Finset.Ico a b, ∑ j in Finset.Ico i b, f i j) =
       ∑ j in Finset.Ico a b, ∑ i in Finset.Ico a (j + 1), f i j := by
   rw [Finset.sum_sigma', Finset.sum_sigma']
-  refine'
-    Finset.sum_bij' (fun (x : Σ _ : ℕ, ℕ) _ => (⟨x.2, x.1⟩ : Σ _ : ℕ, ℕ)) _ (fun _ _ => rfl)
-      (fun (x : Σ _ : ℕ, ℕ) _ => (⟨x.2, x.1⟩ : Σ _ : ℕ, ℕ)) _ (by (rintro ⟨⟩ _; rfl))
-      (by (rintro ⟨⟩ _; rfl)) <;>
+  refine' sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) _ _ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) <;>
   simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
   rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩ <;>
   refine' ⟨⟨_, _⟩, ⟨_, _⟩⟩ <;>

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -140,23 +140,18 @@ theorem prod_add [DecidableEq α] (f g : α → β) (s : Finset α) :
       prod_sum
     _ = ∑ t in s.powerset, (∏ a in t, f a) * ∏ a in s \ t, g a :=
       sum_bij'
-        (fun f _ => s.filter (fun a => ∀ h : a ∈ s, f a h))
-        (by simp)
-        (fun a _ => by
-          rw [prod_ite]
-          congr 1
-          exact prod_bij'
-            (fun a _ => a.1) (by simp) (by simp)
-            (fun a ha => ⟨a, (mem_filter.1 ha).1⟩) (fun a ha => by simp at ha; simp; tauto)
-            (by simp) (by simp)
-          exact prod_bij'
-            (fun a _ => a.1) (by simp) (by simp)
-            (fun a ha => ⟨a, (mem_sdiff.1 ha).1⟩) (fun a ha => by simp at ha; simp; tauto)
-            (by simp) (by simp))
+        (fun f _ ↦ s.filter fun a ↦ ∃ h : a ∈ s, f a h)
         (fun t _ a _ => a ∈ t)
+        (by simp)
         (by simp [Classical.em])
         (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
         (by simp_rw [ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
+        (fun a _ ↦ by
+          simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
+            Subtype.map_coe, id_eq, prod_attach, filter_congr_decidable]
+          congr 2 with x
+          simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
+          tauto)
 #align finset.prod_add Finset.prod_add
 
 /-- `∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j + g j) * (∏ j > i, f j)`. -/

Mathlib/Algebra/BigOperators/Ring.lean

@@ -142,5 +142,5 @@ theorem untrop_sum [ConditionallyCompleteLinearOrder R] [Fintype S] (f : S → T
 as it is simply not true on conditionally complete lattices! -/
 theorem Finset.untrop_sum [ConditionallyCompleteLinearOrder R] (s : Finset S)
     (f : S → Tropical (WithTop R)) : untrop (∑ i in s, f i) = ⨅ i : s, untrop (f i) := by
-  simpa [← _root_.untrop_sum] using sum_attach.symm
+  simpa [← _root_.untrop_sum] using (sum_attach _ _).symm
 #align finset.untrop_sum Finset.untrop_sum

Mathlib/Algebra/Tropical/BigOperators.lean

@@ -90,17 +90,8 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
     simp only [Finset.mem_univ, Finset.compl_filter, Finset.mem_filter, true_and_iff, Fin.val_succ,
       Fin.coe_castLT] at hij ⊢
     linarith
-  · -- identification of corresponding terms in both sums
-    rintro ⟨i, j⟩ hij
-    dsimp
-    simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]
-    congr 1
-    · simp only [Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
-      apply mul_comm
-    · rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
-      simpa using hij
   · -- φ : S → Sᶜ is injective
-    rintro ⟨i, j⟩ ⟨i', j'⟩ hij hij' h
+    rintro ⟨i, j⟩ hij ⟨i', j'⟩ hij' h
     rw [Prod.mk.inj_iff]
     exact ⟨by simpa using congr_arg Prod.snd h,
       by simpa [Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩
@@ -114,6 +105,15 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
     · simpa only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.mem_filter,
         Fin.coe_castSucc, Fin.coe_pred, true_and] using Nat.le_sub_one_of_lt hij'
     · simp only [Fin.castLT_castSucc, Fin.succ_pred]
+  · -- identification of corresponding terms in both sums
+    rintro ⟨i, j⟩ hij
+    dsimp
+    simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]
+    congr 1
+    · simp only [Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
+      apply mul_comm
+    · rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
+      simpa using hij
 #align algebraic_topology.alternating_face_map_complex.d_squared AlgebraicTopology.AlternatingFaceMapComplex.d_squared
 
 /-!

Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

@@ -616,7 +616,7 @@ def compPartialSumTargetSet (m M N : ℕ) : Set (Σ n, Composition n) :=
 
 theorem compPartialSumTargetSet_image_compPartialSumSource (m M N : ℕ)
     (i : Σ n, Composition n) (hi : i ∈ compPartialSumTargetSet m M N) :
-    ∃ (j : _) (hj : j ∈ compPartialSumSource m M N), i = compChangeOfVariables m M N j hj := by
+    ∃ (j : _) (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = i := by
   rcases i with ⟨n, c⟩
   refine' ⟨⟨c.length, c.blocksFun⟩, _, _⟩
   · simp only [compPartialSumTargetSet, Set.mem_setOf_eq] at hi
@@ -625,7 +625,7 @@ theorem compPartialSumTargetSet_image_compPartialSumSource (m M N : ℕ)
   · dsimp [compChangeOfVariables]
     rw [Composition.sigma_eq_iff_blocks_eq]
     simp only [Composition.blocksFun, Composition.blocks, Subtype.coe_eta, List.get_map]
-    conv_lhs => rw [← List.ofFn_get c.blocks]
+    conv_rhs => rw [← List.ofFn_get c.blocks]
 #align formal_multilinear_series.comp_partial_sum_target_subset_image_comp_partial_sum_source FormalMultilinearSeries.compPartialSumTargetSet_image_compPartialSumSource
 
 /-- Target set in the change of variables to compute the composition of partial sums of formal
@@ -665,11 +665,8 @@ theorem compChangeOfVariables_sum {α : Type*} [AddCommMonoid α] (m M N : ℕ)
       map_ofFn, length_ofFn, true_and_iff, compChangeOfVariables]
     intro j
     simp only [Composition.blocksFun, (H.right _).right, List.get_ofFn]
-  -- 2 - show that the composition gives the `comp_along_composition` application
-  · rintro ⟨k, blocks_fun⟩ H
-    rw [h]
-  -- 3 - show that the map is injective
-  · rintro ⟨k, blocks_fun⟩ ⟨k', blocks_fun'⟩ H H' heq
+  -- 2 - show that the map is injective
+  · rintro ⟨k, blocks_fun⟩ H ⟨k', blocks_fun'⟩ H' heq
     obtain rfl : k = k' := by
       have := (compChangeOfVariables_length m M N H).symm
       rwa [heq, compChangeOfVariables_length] at this
@@ -682,10 +679,13 @@ theorem compChangeOfVariables_sum {α : Type*} [AddCommMonoid α] (m M N : ℕ)
         apply Composition.blocksFun_congr <;>
         first | rw [heq] | rfl
       _ = blocks_fun' i := compChangeOfVariables_blocksFun m M N H' i
-  -- 4 - show that the map is surjective
+  -- 3 - show that the map is surjective
   · intro i hi
     apply compPartialSumTargetSet_image_compPartialSumSource m M N i
     simpa [compPartialSumTarget] using hi
+  -- 4 - show that the composition gives the `comp_along_composition` application
+  · rintro ⟨k, blocks_fun⟩ H
+    rw [h]
 #align formal_multilinear_series.comp_change_of_variables_sum FormalMultilinearSeries.compChangeOfVariables_sum
 
 /-- The auxiliary set corresponding to the composition of partial sums asymptotically contains

Mathlib/Analysis/Analytic/Composition.lean

@@ -35,7 +35,8 @@ Together, these four statements say that any two of the following properties imp
 -/
 
 
-open BigOperators
+open Finset
+open scoped BigOperators
 
 namespace Configuration
 
@@ -234,17 +235,11 @@ theorem HasLines.card_le [HasLines P L] [Fintype P] [Fintype L] :
       ∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
       _ ≤ ∑ l, lineCount L (f l) :=
         (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
-      _ = ∑ p in Finset.univ.image f, lineCount L p :=
-        (Finset.sum_bij (fun l _ => f l) (fun l hl => Finset.mem_image_of_mem f hl)
-          (fun l _ => rfl) (fun l₁ l₂ hl₁ hl₂ hl₃ => hf₁ hl₃) fun p => by
-          rw [Finset.mem_image]
-          exact fun ⟨a, ⟨h, h'⟩⟩ => ⟨a, ⟨h, h'.symm⟩⟩)
+      _ = ∑ p in univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
       _ < ∑ p, lineCount L p := by
         obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
-        refine'
-          Finset.sum_lt_sum_of_subset (Finset.univ.image f).subset_univ (Finset.mem_univ p) _ _
-            fun p _ _ => zero_le (lineCount L p)
-        · simpa only [Finset.mem_image, exists_prop, Finset.mem_univ, true_and_iff]
+        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le _
+        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and_iff]
         · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
           obtain ⟨l, _⟩ := @exists_line P L _ _ p
           exact
@@ -267,16 +262,8 @@ theorem HasLines.exists_bijective_of_card_eq [HasLines P L] [Fintype P] [Fintype
   classical
     obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
     have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
-    refine'
-      ⟨f, hf3, fun l =>
-        (Finset.sum_eq_sum_iff_of_le fun l _ => HasLines.pointCount_le_lineCount (hf2 l)).mp
-          ((sum_lineCount_eq_sum_pointCount P L).symm.trans
-            (Finset.sum_bij (fun l _ => f l) (fun l _ => Finset.mem_univ (f l))
-                (fun l _ => refl (lineCount L (f l))) (fun l₁ l₂ hl₁ hl₂ hl => hf1 hl) fun p hp =>
-                _).symm)
-          l (Finset.mem_univ l)⟩
-    obtain ⟨l, rfl⟩ := hf3.2 p
-    exact ⟨l, Finset.mem_univ l, rfl⟩
+    exact ⟨f, hf3, fun l ↦ (sum_eq_sum_iff_of_le fun l _ ↦ pointCount_le_lineCount (hf2 l)).1
+          ((hf3.sum_comp _).trans (sum_lineCount_eq_sum_pointCount P L)).symm _ $ mem_univ _⟩
 #align configuration.has_lines.exists_bijective_of_card_eq Configuration.HasLines.exists_bijective_of_card_eq
 
 theorem HasLines.lineCount_eq_pointCount [HasLines P L] [Fintype P] [Fintype L]
@@ -290,15 +277,11 @@ theorem HasLines.lineCount_eq_pointCount [HasLines P L] [Fintype P] [Fintype L]
       simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
     have step2 : ∑ i in s, lineCount L i.1 = ∑ i in s, pointCount P i.2 := by
       rw [s.sum_finset_product Finset.univ fun p => Set.toFinset { l | p ∈ l }]
-      rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }]
-      refine'
-        (Finset.sum_bij (fun l _ => f l) (fun l _ => Finset.mem_univ (f l)) (fun l hl => _)
-            (fun _ _ _ _ h => hf1.1 h) fun p _ => _).symm
-      · simp_rw [Finset.sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
-        change pointCount P l • pointCount P l = lineCount L (f l) • lineCount L (f l)
-        rw [hf2]
-      · obtain ⟨l, hl⟩ := hf1.2 p
-        exact ⟨l, Finset.mem_univ l, hl.symm⟩
+      rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset { p | p ∈ l }, eq_comm]
+      refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
+      simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
+      change pointCount P l • _ = lineCount L (f l) • _
+      rw [hf2]
       all_goals simp_rw [Finset.mem_univ, true_and_iff, Set.mem_toFinset]; exact fun p => Iff.rfl
     have step3 : ∑ i in sᶜ, lineCount L i.1 = ∑ i in sᶜ, pointCount P i.2 := by
       rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1

Mathlib/Combinatorics/Configuration.lean

@@ -187,31 +187,12 @@ theorem sum_range_diag_flip {α : Type*} [AddCommMonoid α] (n : ℕ) (f : ℕ 
     (∑ m in range n, ∑ k in range (m + 1), f k (m - k)) =
       ∑ m in range n, ∑ k in range (n - m), f m k := by
   rw [sum_sigma', sum_sigma']
-  exact
-    sum_bij (fun a _ => ⟨a.2, a.1 - a.2⟩)
-      (fun a ha =>
-        have h₁ : a.1 < n := mem_range.1 (mem_sigma.1 ha).1
-        have h₂ : a.2 < Nat.succ a.1 := mem_range.1 (mem_sigma.1 ha).2
-        mem_sigma.2
-          ⟨mem_range.2 (lt_of_lt_of_le h₂ h₁),
-            mem_range.2 ((tsub_lt_tsub_iff_right (Nat.le_of_lt_succ h₂)).2 h₁)⟩)
-      (fun _ _ => rfl)
-      (fun ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h =>
-        have ha : a₁ < n ∧ a₂ ≤ a₁ :=
-          ⟨mem_range.1 (mem_sigma.1 ha).1, Nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 ha).2)⟩
-        have hb : b₁ < n ∧ b₂ ≤ b₁ :=
-          ⟨mem_range.1 (mem_sigma.1 hb).1, Nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 hb).2)⟩
-        have h : a₂ = b₂ ∧ _ := by simpa using h
-        have h' : a₁ = b₁ - b₂ + a₂ := (tsub_eq_iff_eq_add_of_le ha.2).1 (eq_of_heq h.2)
-        Sigma.mk.inj_iff.2 ⟨tsub_add_cancel_of_le hb.2 ▸ h'.symm ▸ h.1 ▸ rfl, heq_of_eq h.1⟩)
-      fun ⟨a₁, a₂⟩ ha =>
-      have ha : a₁ < n ∧ a₂ < n - a₁ :=
-        ⟨mem_range.1 (mem_sigma.1 ha).1, mem_range.1 (mem_sigma.1 ha).2⟩
-      ⟨⟨a₂ + a₁, a₁⟩,
-        ⟨mem_sigma.2
-            ⟨mem_range.2 (lt_tsub_iff_right.1 ha.2),
-              mem_range.2 (Nat.lt_succ_of_le (Nat.le_add_left _ _))⟩,
-          Sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (add_tsub_cancel_right _ _).symm⟩⟩⟩
+  refine sum_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
+    simp (config := { contextual := true }) only [mem_sigma, mem_range, lt_tsub_iff_left,
+      Nat.lt_succ_iff, le_add_iff_nonneg_right, zero_le, and_true, and_imp, imp_self, implies_true,
+      Sigma.forall, forall_const, add_tsub_cancel_of_le, Sigma.mk.inj_iff,
+      add_tsub_cancel_left, heq_eq_eq]
+  · exact fun a b han hba ↦ lt_of_le_of_lt hba han
 #align sum_range_diag_flip sum_range_diag_flip
 
 end
@@ -1602,20 +1583,9 @@ theorem sum_div_factorial_le {α : Type*} [LinearOrderedField α] (n j : ℕ) (h
       (1 / m.factorial : α)) ≤ n.succ / (n.factorial * n) :=
   calc
     (∑ m in filter (fun k => n ≤ k) (range j), (1 / m.factorial : α)) =
-        ∑ m in range (j - n), (1 / ((m + n).factorial : α)) :=
-      sum_bij (fun m _ => m - n)
-        (fun m hm =>
-          mem_range.2 <|
-            (tsub_lt_tsub_iff_right (by simp at hm; tauto)).2 (by simp at hm; tauto))
-        (fun m hm => by rw [tsub_add_cancel_of_le]; simp at *; tauto)
-        (fun a₁ a₂ ha₁ ha₂ h => by
-          rwa [tsub_eq_iff_eq_add_of_le, tsub_add_eq_add_tsub, eq_comm, tsub_eq_iff_eq_add_of_le,
-              add_left_inj, eq_comm] at h <;>
-          simp at * <;> aesop)
-        fun b hb =>
-        ⟨b + n,
-          mem_filter.2 ⟨mem_range.2 <| lt_tsub_iff_right.mp (mem_range.1 hb), Nat.le_add_left _ _⟩,
-          by dsimp; rw [add_tsub_cancel_right]⟩
+        ∑ m in range (j - n), (1 / ((m + n).factorial : α)) := by
+        refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_ <;>
+          simp (config := { contextual := true }) [lt_tsub_iff_right, tsub_add_cancel_of_le]
     _ ≤ ∑ m in range (j - n), ((n.factorial : α) * (n.succ : α) ^ m)⁻¹ := by
       simp_rw [one_div]
       gcongr