diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
index 7c252a8743dfa..9a4a252031c9c 100644
--- a/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -537,73 +537,165 @@ theorem prod_sigma' {σ : α → Type*} (s : Finset α) (t : ∀ a, Finset (σ a
 #align finset.prod_sigma' Finset.prod_sigma'
 #align finset.sum_sigma' Finset.sum_sigma'
 
+section bij
+variable {ι κ α : Type*} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α}
+
 /-- Reorder a product.
 
-  The difference with `prod_bij'` is that the bijection is specified as a surjective injection,
-  rather than by an inverse function.
--/
+The difference with `Finset.prod_bij'` is that the bijection is specified as a surjective injection,
+rather than by an inverse function.
+
+The difference with `Finset.prod_nbij` is that the bijection is allowed to use membership of the
+domain of the product, rather than being a non-dependent function. -/
 @[to_additive "Reorder a sum.
 
-  The difference with `sum_bij'` is that the bijection is specified as a surjective injection,
-  rather than by an inverse function."]
-theorem prod_bij {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (i : ∀ a ∈ s, γ)
-    (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
-    (i_inj : ∀ a₁ a₂ ha₁ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
-    (i_surj : ∀ b ∈ t, ∃ a ha, b = i a ha) : ∏ x in s, f x = ∏ x in t, g x :=
-  congr_arg Multiset.prod (Multiset.map_eq_map_of_bij_of_nodup f g s.2 t.2 i hi h i_inj i_surj)
+The difference with `Finset.sum_bij'` is that the bijection is specified as a surjective injection,
+rather than by an inverse function.
+
+The difference with `Finset.sum_nbij` is that the bijection is allowed to use membership of the
+domain of the sum, rather than being a non-dependent function."]
+theorem prod_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t)
+    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
+    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) :
+    ∏ x in s, f x = ∏ x in t, g x :=
+  congr_arg Multiset.prod (Multiset.map_eq_map_of_bij_of_nodup f g s.2 t.2 i hi i_inj i_surj h)
 #align finset.prod_bij Finset.prod_bij
 #align finset.sum_bij Finset.sum_bij
 
 /-- Reorder a product.
 
-  The difference with `prod_bij` is that the bijection is specified with an inverse, rather than
-  as a surjective injection.
--/
+The difference with `Finset.prod_bij` is that the bijection is specified with an inverse, rather
+than as a surjective injection.
+
+The difference with `Finset.prod_nbij'` is that the bijection and its inverse are allowed to use
+membership of the domains of the products, rather than being non-dependent functions. -/
 @[to_additive "Reorder a sum.
 
-  The difference with `sum_bij` is that the bijection is specified with an inverse, rather than
-  as a surjective injection."]
-theorem prod_bij' {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (i : ∀ a ∈ s, γ)
-    (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha)) (j : ∀ a ∈ t, α)
+The difference with `Finset.sum_bij` is that the bijection is specified with an inverse, rather than
+as a surjective injection.
+
+The difference with `Finset.sum_nbij'` is that the bijection and its inverse are allowed to use
+membership of the domains of the sums, rather than being non-dependent functions."]
+theorem prod_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t)
     (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
-    (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) : ∏ x in s, f x = ∏ x in t, g x := by
-  refine' prod_bij i hi h _ _
-  · intro a1 a2 h1 h2 eq
-    rw [← left_inv a1 h1, ← left_inv a2 h2]
-    simp only [eq]
-  · intro b hb
-    use j b hb
-    use hj b hb
-    exact (right_inv b hb).symm
+    (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) (h : ∀ a ha, f a = g (i a ha)) :
+    ∏ x in s, f x = ∏ x in t, g x := by
+  refine prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h
+  rw [← left_inv a1 h1, ← left_inv a2 h2]
+  simp only [eq]
 #align finset.prod_bij' Finset.prod_bij'
 #align finset.sum_bij' Finset.sum_bij'
 
-/-- Reindexing a product over a finset along an equivalence.
-See `Equiv.prod_comp` for the version where `s` and `s'` are `univ`. -/
-@[to_additive " Reindexing a sum over a finset along an equivalence.
-See `Equiv.sum_comp` for the version where `s` and `s'` are `univ`. "]
-theorem Equiv.prod_comp_finset {ι'} [DecidableEq ι] (e : ι ≃ ι') (f : ι' → β) {s' : Finset ι'}
-    {s : Finset ι} (h : s = s'.image e.symm) : ∏ i' in s', f i' = ∏ i in s, f (e i) := by
-  rw [h]
-  refine'
-    Finset.prod_bij' (fun i' _hi' => e.symm i') (fun a ha => Finset.mem_image_of_mem _ ha)
-      (fun a _ha => by simp_rw [e.apply_symm_apply]) (fun i _hi => e i) (fun a ha => _)
-      (fun a _ha => e.apply_symm_apply a) fun a _ha => e.symm_apply_apply a
-  rcases Finset.mem_image.mp ha with ⟨i', hi', rfl⟩
-  dsimp only
-  rwa [e.apply_symm_apply]
-#align finset.equiv.prod_comp_finset Finset.Equiv.prod_comp_finset
-#align finset.equiv.sum_comp_finset Finset.Equiv.sum_comp_finset
+/-- Reorder a product.
+
+The difference with `Finset.prod_nbij'` is that the bijection is specified as a surjective
+injection, rather than by an inverse function.
+
+The difference with `Finset.prod_bij` is that the bijection is a non-dependent function, rather than
+being allowed to use membership of the domain of the product. -/
+@[to_additive "Reorder a sum.
+
+The difference with `Finset.sum_nbij'` is that the bijection is specified as a surjective injection,
+rather than by an inverse function.
+
+The difference with `Finset.sum_bij` is that the bijection is a non-dependent function, rather than
+being allowed to use membership of the domain of the sum."]
+lemma prod_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : (s : Set ι).InjOn i)
+    (i_surj : (s : Set ι).SurjOn i t) (h : ∀ a ∈ s, f a = g (i a)) :
+    ∏ x in s, f x = ∏ x in t, g x :=
+  prod_bij (fun a _ ↦ i a) hi i_inj (by simpa using i_surj) h
+
+/-- Reorder a product.
+
+The difference with `Finset.prod_nbij` is that the bijection is specified with an inverse, rather
+than as a surjective injection.
+
+The difference with `Finset.prod_bij'` is that the bijection and its inverse are non-dependent
+functions, rather than being allowed to use membership of the domains of the products.
+
+The difference with `Finset.prod_equiv` is that bijectivity is only required to hold on the domains
+of the products, rather than on the entire types.
+-/
+@[to_additive "Reorder a sum.
+
+The difference with `Finset.sum_nbij` is that the bijection is specified with an inverse, rather
+than as a surjective injection.
+
+The difference with `Finset.sum_bij'` is that the bijection and its inverse are non-dependent
+functions, rather than being allowed to use membership of the domains of the sums.
+
+The difference with `Finset.sum_equiv` is that bijectivity is only required to hold on the domains
+of the sums, rather than on the entire types."]
+lemma prod_nbij' (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s)
+    (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a)
+    (h : ∀ a ∈ s, f a = g (i a)) : ∏ x in s, f x = ∏ x in t, g x :=
+  prod_bij' (fun a _ ↦ i a) (fun b _ ↦ j b) hi hj left_inv right_inv h
+
+/-- Specialization of `Finset.prod_nbij'` that automatically fills in most arguments.
+
+See `Fintype.prod_equiv` for the version where `s` and `t` are `univ`. -/
+@[to_additive "`Specialization of `Finset.sum_nbij'` that automatically fills in most arguments.
+
+See `Fintype.sum_equiv` for the version where `s` and `t` are `univ`."]
+lemma prod_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
+    ∏ i in s, f i = ∏ i in t, g i := by refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg <;> simp [hst]
+#align finset.equiv.prod_comp_finset Finset.prod_equiv
+#align finset.equiv.sum_comp_finset Finset.sum_equiv
+
+/-- Specialization of `Finset.prod_bij` that automatically fills in most arguments.
+
+See `Fintype.prod_bijective` for the version where `s` and `t` are `univ`. -/
+@[to_additive "`Specialization of `Finset.sum_bij` that automatically fills in most arguments.
+
+See `Fintype.sum_bijective` for the version where `s` and `t` are `univ`."]
+lemma prod_bijective (e : ι → κ) (he : e.Bijective) (hst : ∀ i, i ∈ s ↔ e i ∈ t)
+    (hfg : ∀ i ∈ s, f i = g (e i)) :
+    ∏ i in s, f i = ∏ i in t, g i := prod_equiv (.ofBijective e he) hst hfg
+
+variable [DecidableEq κ]
+
+@[to_additive]
+lemma prod_fiberwise_of_maps_to {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → α) :
+    ∏ j in t, ∏ i in s.filter fun i ↦ g i = j, f i = ∏ i in s, f i := by
+  rw [← prod_disjiUnion, disjiUnion_filter_eq_of_maps_to h]
+#align finset.prod_fiberwise_of_maps_to Finset.prod_fiberwise_of_maps_to
+#align finset.sum_fiberwise_of_maps_to Finset.sum_fiberwise_of_maps_to
+
+@[to_additive]
+lemma prod_fiberwise_of_maps_to' {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → α) :
+    ∏ j in t, ∏ _i in s.filter fun i ↦ g i = j, f j = ∏ i in s, f (g i) := by
+  calc
+    _ = ∏ y in t, ∏ x in s.filter fun x ↦ g x = y, f (g x) :=
+        prod_congr rfl $ fun y _ ↦ prod_congr rfl fun x hx ↦ by rw [(mem_filter.1 hx).2]
+    _ = _ := prod_fiberwise_of_maps_to h _
+
+variable [Fintype κ]
+
+@[to_additive]
+lemma prod_fiberwise (s : Finset ι) (g : ι → κ) (f : ι → α) :
+    ∏ j, ∏ i in s.filter fun i ↦ g i = j, f i = ∏ i in s, f i :=
+  prod_fiberwise_of_maps_to (fun _ _ ↦ mem_univ _) _
+#align finset.prod_fiberwise Finset.prod_fiberwise
+#align finset.sum_fiberwise Finset.sum_fiberwise
+
+@[to_additive]
+lemma prod_fiberwise' (s : Finset ι) (g : ι → κ) (f : κ → α) :
+    ∏ j, ∏ _i in s.filter fun i ↦ g i = j, f j = ∏ i in s, f (g i) :=
+  prod_fiberwise_of_maps_to' (fun _ _ ↦ mem_univ _) _
+
+end bij
+
+@[to_additive (attr := simp)]
+lemma prod_diag [DecidableEq α] (s : Finset α) (f : α × α → β) :
+    ∏ i in s.diag, f i = ∏ i in s, f (i, i) := by
+  apply prod_nbij' Prod.fst (fun i ↦ (i, i)) <;> simp
 
 @[to_additive]
 theorem prod_finset_product (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α)
     (h : ∀ p : γ × α, p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} :
     ∏ p in r, f p = ∏ c in s, ∏ a in t c, f (c, a) := by
   refine' Eq.trans _ (prod_sigma s t fun p => f (p.1, p.2))
-  exact
-    prod_bij' (fun p _hp => ⟨p.1, p.2⟩) (fun p => mem_sigma.mpr ∘ (h p).mp)
-      (fun p _ => rfl) (fun p _hp => (p.1, p.2))
-      (fun p => (h (p.1, p.2)).mpr ∘ mem_sigma.mp) (fun p _ => rfl) fun p _hp => p.eta
+  apply prod_equiv (Equiv.sigmaEquivProd _ _).symm <;> simp [h]
 #align finset.prod_finset_product Finset.prod_finset_product
 #align finset.sum_finset_product Finset.sum_finset_product
 
@@ -620,10 +712,7 @@ theorem prod_finset_product_right (r : Finset (α × γ)) (s : Finset γ) (t : 
     (h : ∀ p : α × γ, p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} :
     ∏ p in r, f p = ∏ c in s, ∏ a in t c, f (a, c) := by
   refine' Eq.trans _ (prod_sigma s t fun p => f (p.2, p.1))
-  exact
-    prod_bij' (fun p _hp => ⟨p.2, p.1⟩) (fun p => mem_sigma.mpr ∘ (h p).mp)
-      (fun p _c => rfl) (fun p _hp => (p.2, p.1))
-      (fun p => (h (p.2, p.1)).mpr ∘ mem_sigma.mp) (fun p _ => rfl) fun p _hp => p.eta
+  apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm) <;> simp [h]
 #align finset.prod_finset_product_right Finset.prod_finset_product_right
 #align finset.sum_finset_product_right Finset.sum_finset_product_right
 
@@ -635,14 +724,6 @@ theorem prod_finset_product_right' (r : Finset (α × γ)) (s : Finset γ) (t :
 #align finset.prod_finset_product_right' Finset.prod_finset_product_right'
 #align finset.sum_finset_product_right' Finset.sum_finset_product_right'
 
-@[to_additive]
-theorem prod_fiberwise_of_maps_to [DecidableEq γ] {s : Finset α} {t : Finset γ} {g : α → γ}
-    (h : ∀ x ∈ s, g x ∈ t) (f : α → β) :
-    (∏ y in t, ∏ x in s.filter fun x => g x = y, f x) = ∏ x in s, f x := by
-  rw [← prod_disjiUnion, disjiUnion_filter_eq_of_maps_to h]
-#align finset.prod_fiberwise_of_maps_to Finset.prod_fiberwise_of_maps_to
-#align finset.sum_fiberwise_of_maps_to Finset.sum_fiberwise_of_maps_to
-
 @[to_additive]
 theorem prod_image' [DecidableEq α] {s : Finset γ} {g : γ → α} (h : γ → β)
     (eq : ∀ c ∈ s, f (g c) = ∏ x in s.filter fun c' => g c' = g c, h x) :
@@ -662,6 +743,11 @@ theorem prod_mul_distrib : ∏ x in s, f x * g x = (∏ x in s, f x) * ∏ x in
 #align finset.prod_mul_distrib Finset.prod_mul_distrib
 #align finset.sum_add_distrib Finset.sum_add_distrib
 
+@[to_additive]
+lemma prod_mul_prod_comm (f g h i : α → β) :
+    (∏ a in s, f a * g a) * ∏ a in s, h a * i a = (∏ a in s, f a * h a) * ∏ a in s, g a * i a := by
+  simp_rw [prod_mul_distrib, mul_mul_mul_comm]
+
 @[to_additive]
 theorem prod_product {s : Finset γ} {t : Finset α} {f : γ × α → β} :
     ∏ x in s ×ˢ t, f x = ∏ x in s, ∏ y in t, f (x, y) :=
@@ -807,6 +893,16 @@ theorem prod_eq_single {s : Finset α} {f : α → β} (a : α) (h₀ : ∀ b 
 #align finset.prod_eq_single Finset.prod_eq_single
 #align finset.sum_eq_single Finset.sum_eq_single
 
+@[to_additive]
+lemma prod_union_eq_left [DecidableEq α] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1) :
+    ∏ a in s₁ ∪ s₂, f a = ∏ a in s₁, f a :=
+  Eq.symm $
+    prod_subset (subset_union_left _ _) fun _a ha ha' ↦ hs _ ((mem_union.1 ha).resolve_left ha') ha'
+
+@[to_additive]
+lemma prod_union_eq_right [DecidableEq α] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) :
+    ∏ a in s₁ ∪ s₂, f a = ∏ a in s₂, f a := by rw [union_comm, prod_union_eq_left hs]
+
 @[to_additive]
 theorem prod_eq_mul_of_mem {s : Finset α} {f : α → β} (a b : α) (ha : a ∈ s) (hb : b ∈ s)
     (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : ∏ x in s, f x = f a * f b := by
@@ -851,7 +947,7 @@ theorem prod_eq_mul {s : Finset α} {f : α → β} (a b : α) (hn : a ≠ b)
 #align finset.sum_eq_add Finset.sum_eq_add
 
 @[to_additive]
-theorem prod_attach {f : α → β} : ∏ x in s.attach, f x = ∏ x in s, f x :=
+theorem prod_attach (s : Finset α) (f : α → β) : ∏ x in s.attach, f x = ∏ x in s, f x :=
   haveI := Classical.decEq α
   calc
     ∏ x in s.attach, f x.val = ∏ x in s.attach.image Subtype.val, f x := by
@@ -905,8 +1001,7 @@ theorem prod_coe_sort_eq_attach (f : s → β) : ∏ i : s, f i = ∏ i in s.att
 #align finset.sum_coe_sort_eq_attach Finset.sum_coe_sort_eq_attach
 
 @[to_additive]
-theorem prod_coe_sort : ∏ i : s, f i = ∏ i in s, f i :=
-  prod_attach
+theorem prod_coe_sort : ∏ i : s, f i = ∏ i in s, f i := prod_attach _ _
 #align finset.prod_coe_sort Finset.prod_coe_sort
 #align finset.sum_coe_sort Finset.sum_coe_sort
 
@@ -964,7 +1059,7 @@ theorem prod_apply_dite {s : Finset α} {p : α → Prop} {hp : DecidablePred p}
       (prod_filter_mul_prod_filter_not s p _).symm
     _ = (∏ x in (s.filter p).attach, h (if hx : p x.1 then f x.1 hx else g x.1 hx)) *
           ∏ x in (s.filter fun x => ¬p x).attach, h (if hx : p x.1 then f x.1 hx else g x.1 hx) :=
-      congr_arg₂ _ prod_attach.symm prod_attach.symm
+      congr_arg₂ _ (prod_attach _ _).symm (prod_attach _ _).symm
     _ = (∏ x in (s.filter p).attach, h (f x.1 $ by simpa using (mem_filter.mp x.2).2)) *
           ∏ x in (s.filter fun x ↦ ¬p x).attach, h (g x.1 $ by simpa using (mem_filter.mp x.2).2) :=
       congr_arg₂ _ (prod_congr rfl fun x _hx ↦
@@ -978,8 +1073,7 @@ theorem prod_apply_ite {s : Finset α} {p : α → Prop} {_hp : DecidablePred p}
     (h : γ → β) :
     (∏ x in s, h (if p x then f x else g x)) =
       (∏ x in s.filter p, h (f x)) * ∏ x in s.filter fun x => ¬p x, h (g x) :=
-  _root_.trans (prod_apply_dite _ _ _)
-    (congr_arg₂ _ (@prod_attach _ _ _ _ (h ∘ f)) (@prod_attach _ _ _ _ (h ∘ g)))
+  (prod_apply_dite _ _ _).trans $ congr_arg₂ _ (prod_attach _ (h ∘ f)) (prod_attach _ (h ∘ g))
 #align finset.prod_apply_ite Finset.prod_apply_ite
 #align finset.sum_apply_ite Finset.sum_apply_ite
 
@@ -1192,6 +1286,11 @@ lemma prod_mulIndicator_eq_prod_filter (s : Finset ι) (f : ι → κ → β) (t
 #align finset.prod_mul_indicator_eq_prod_filter Finset.prod_mulIndicator_eq_prod_filter
 #align finset.sum_indicator_eq_sum_filter Finset.sum_indicator_eq_sum_filter
 
+@[to_additive]
+lemma prod_mulIndicator_eq_prod_inter [DecidableEq ι] (s t : Finset ι) (f : ι → β) :
+    ∏ i in s, (t : Set ι).mulIndicator f i = ∏ i in s ∩ t, f i := by
+  rw [← filter_mem_eq_inter, prod_mulIndicator_eq_prod_filter]; rfl
+
 @[to_additive]
 lemma mulIndicator_prod (s : Finset ι) (t : Set κ) (f : ι → κ → β) :
     mulIndicator t (∏ i in s, f i) = ∏ i in s, mulIndicator t (f i) :=
@@ -1227,8 +1326,8 @@ end indicator
 @[to_additive]
 theorem prod_bij_ne_one {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β}
     (i : ∀ a ∈ s, f a ≠ 1 → γ) (hi : ∀ a h₁ h₂, i a h₁ h₂ ∈ t)
-    (i_inj : ∀ a₁ a₂ h₁₁ h₁₂ h₂₁ h₂₂, i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
-    (i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a h₁ h₂, b = i a h₁ h₂) (h : ∀ a h₁ h₂, f a = g (i a h₁ h₂)) :
+    (i_inj : ∀ a₁ h₁₁ h₁₂ a₂ h₂₁ h₂₂, i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
+    (i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a h₁ h₂, i a h₁ h₂ = b) (h : ∀ a h₁ h₂, f a = g (i a h₁ h₂)) :
     ∏ x in s, f x = ∏ x in t, g x := by
   classical
   calc
@@ -1243,9 +1342,7 @@ theorem prod_bij_ne_one {s : Finset α} {t : Finset γ} {f : α → β} {g : γ
     refine (mem_filter.mpr ⟨hi a h₁ _, ?_⟩)
     specialize h a h₁ fun H ↦ by rw [H] at h₂; simp at h₂
     rwa [← h]
-  · refine' (fun a ha => (mem_filter.mp ha).elim fun h₁ h₂ ↦ _)
-    exact h a h₁ fun H ↦ by rw [H] at h₂; simp at h₂
-  · intros a₁ a₂ ha₁ ha₂
+  · intros a₁ ha₁ a₂ ha₂
     refine' (mem_filter.mp ha₁).elim fun _ha₁₁ _ha₁₂ ↦ _
     refine' (mem_filter.mp ha₂).elim fun _ha₂₁ _ha₂₂ ↦ _
     apply i_inj
@@ -1253,30 +1350,24 @@ theorem prod_bij_ne_one {s : Finset α} {t : Finset γ} {f : α → β} {g : γ
     refine' (mem_filter.mp hb).elim fun h₁ h₂ ↦ _
     obtain ⟨a, ha₁, ha₂, eq⟩ := i_surj b h₁ fun H ↦ by rw [H] at h₂; simp at h₂
     exact ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩
+  · refine' (fun a ha => (mem_filter.mp ha).elim fun h₁ h₂ ↦ _)
+    exact h a h₁ fun H ↦ by rw [H] at h₂; simp at h₂
 #align finset.prod_bij_ne_one Finset.prod_bij_ne_one
 #align finset.sum_bij_ne_zero Finset.sum_bij_ne_zero
 
 @[to_additive]
 theorem prod_dite_of_false {p : α → Prop} {hp : DecidablePred p} (h : ∀ x ∈ s, ¬p x)
     (f : ∀ x : α, p x → β) (g : ∀ x : α, ¬p x → β) :
-    ∏ x in s, (if hx : p x then f x hx else g x hx) = ∏ x : s, g x.val (h x.val x.property) :=
-  prod_bij (fun x hx => ⟨x, hx⟩) (fun x hx => by simp)
-    (fun a ha => by
-      dsimp
-      rw [dif_neg])
-    (fun a₁ a₂ h₁ h₂ hh => congr_arg Subtype.val hh) fun b _hb => ⟨b.1, b.2, by simp⟩
+    ∏ x in s, (if hx : p x then f x hx else g x hx) = ∏ x : s, g x.val (h x.val x.property) := by
+  refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop
 #align finset.prod_dite_of_false Finset.prod_dite_of_false
 #align finset.sum_dite_of_false Finset.sum_dite_of_false
 
 @[to_additive]
 theorem prod_dite_of_true {p : α → Prop} {hp : DecidablePred p} (h : ∀ x ∈ s, p x)
     (f : ∀ x : α, p x → β) (g : ∀ x : α, ¬p x → β) :
-    ∏ x in s, (if hx : p x then f x hx else g x hx) = ∏ x : s, f x.val (h x.val x.property) :=
-  prod_bij (fun x hx => ⟨x, hx⟩) (fun x hx => by simp)
-    (fun a ha => by
-      dsimp
-      rw [dif_pos])
-    (fun a₁ a₂ h₁ h₂ hh => congr_arg Subtype.val hh) fun b _hb => ⟨b.1, b.2, by simp⟩
+    ∏ x in s, (if hx : p x then f x hx else g x hx) = ∏ x : s, f x.val (h x.val x.property) := by
+  refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop
 #align finset.prod_dite_of_true Finset.prod_dite_of_true
 #align finset.sum_dite_of_true Finset.sum_dite_of_true
 
@@ -1429,12 +1520,9 @@ theorem prod_multiset_count_of_subset [DecidableEq α] [CommMonoid α] (m : Mult
 
 @[to_additive]
 theorem prod_mem_multiset [DecidableEq α] (m : Multiset α) (f : { x // x ∈ m } → β) (g : α → β)
-    (hfg : ∀ x, f x = g x) : ∏ x : { x // x ∈ m }, f x = ∏ x in m.toFinset, g x :=
-  prod_bij (fun x _ => x.1) (fun x _ => Multiset.mem_toFinset.mpr x.2) (fun _ _ => hfg _)
-    (fun _ _ _ _ h => by
-      ext
-      assumption)
-    fun y hy => ⟨⟨y, Multiset.mem_toFinset.mp hy⟩, Finset.mem_univ _, rfl⟩
+    (hfg : ∀ x, f x = g x) : ∏ x : { x // x ∈ m }, f x = ∏ x in m.toFinset, g x := by
+  refine' prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_ <;>
+    simp [hfg]
 #align finset.prod_mem_multiset Finset.prod_mem_multiset
 #align finset.sum_mem_multiset Finset.sum_mem_multiset
 
@@ -1618,20 +1706,8 @@ theorem prod_involution {s : Finset α} {f : α → β} :
 @[to_additive "The sum of the composition of functions `f` and `g`, is the sum over `b ∈ s.image g`
 of `f b` times of the cardinality of the fibre of `b`. See also `Finset.sum_image`."]
 theorem prod_comp [DecidableEq γ] (f : γ → β) (g : α → γ) :
-    (∏ a in s, f (g a)) = ∏ b in s.image g, f b ^ (s.filter fun a => g a = b).card :=
-  calc
-    (∏ a in s, f (g a)) =
-        ∏ x in (s.image g).sigma fun b : γ => s.filter fun a => g a = b, f (g x.2) :=
-      prod_bij (fun a _ha => ⟨g a, a⟩) (by simp; tauto) (fun _ _ => rfl) (by simp)
-        (by -- `(by finish)` closes this
-          rintro ⟨b_fst, b_snd⟩ H
-          simp only [mem_image, exists_prop, mem_filter, mem_sigma, decide_eq_true_eq] at H
-          tauto)
-    _ = ∏ b in s.image g, ∏ a in s.filter fun a => g a = b, f (g a) := prod_sigma _ _ _
-    _ = ∏ b in s.image g, ∏ _a in s.filter fun a => g a = b, f b :=
-      prod_congr rfl fun b _hb => prod_congr rfl (by simp (config := { contextual := true }))
-    _ = ∏ b in s.image g, f b ^ (s.filter fun a => g a = b).card :=
-      prod_congr rfl fun _ _ => prod_const _
+    ∏ a in s, f (g a) = ∏ b in s.image g, f b ^ (s.filter fun a => g a = b).card := by
+  simp_rw [← prod_const, prod_fiberwise_of_maps_to' fun _ ↦ mem_image_of_mem _]
 #align finset.prod_comp Finset.prod_comp
 #align finset.sum_comp Finset.sum_comp
 
@@ -1782,12 +1858,13 @@ theorem prod_erase [DecidableEq α] (s : Finset α) {f : α → β} {a : α} (h
 
 /-- See also `Finset.prod_boole`. -/
 @[to_additive "See also `Finset.sum_boole`."]
-theorem prod_ite_one {f : α → Prop} [DecidablePred f] (hf : (s : Set α).PairwiseDisjoint f)
-    (a : β) : (∏ i in s, ite (f i) a 1) = ite (∃ i ∈ s, f i) a 1 := by
+theorem prod_ite_one (s : Finset α) (p : α → Prop) [DecidablePred p]
+    (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) :
+    ∏ i in s, ite (p i) a 1 = ite (∃ i ∈ s, p i) a 1 := by
   split_ifs with h
-  · obtain ⟨i, hi, hfi⟩ := h
-    rw [prod_eq_single_of_mem _ hi, if_pos hfi]
-    exact fun j hj h => if_neg fun hfj => (hf hj hi h).le_bot ⟨hfj, hfi⟩
+  · obtain ⟨i, hi, hpi⟩ := h
+    rw [prod_eq_single_of_mem _ hi, if_pos hpi]
+    exact fun j hj hji ↦ if_neg fun hpj ↦ hji $ h _ hj _ hi hpj hpi
   · push_neg at h
     rw [prod_eq_one]
     exact fun i hi => if_neg (h i hi)
@@ -2086,6 +2163,7 @@ theorem prod_int_mod (s : Finset α) (n : ℤ) (f : α → ℤ) :
 end Finset
 
 namespace Fintype
+variable {ι κ α : Type*} [Fintype ι] [Fintype κ] [CommMonoid α]
 
 open Finset
 
@@ -2096,17 +2174,13 @@ See `Function.Bijective.prod_comp` for a version without `h`. -/
 `Function.Bijective`.
 
 See `Function.Bijective.sum_comp` for a version without `h`. "]
-theorem prod_bijective {α β M : Type*} [Fintype α] [Fintype β] [CommMonoid M] (e : α → β)
-    (he : Function.Bijective e) (f : α → M) (g : β → M) (h : ∀ x, f x = g (e x)) :
-    ∏ x : α, f x = ∏ x : β, g x :=
-  prod_bij (fun x _ => e x) (fun x _ => mem_univ (e x)) (fun x _ => h x)
-    (fun _x _x' _ _ h => he.injective h) fun y _ =>
-    (he.surjective y).imp fun _a h => ⟨mem_univ _, h.symm⟩
+lemma prod_bijective (e : ι → κ) (he : e.Bijective) (f : ι → α) (g : κ → α)
+    (h : ∀ x, f x = g (e x)) : ∏ x, f x = ∏ x, g x :=
+  prod_equiv (.ofBijective e he) (by simp) (by simp [h])
 #align fintype.prod_bijective Fintype.prod_bijective
 #align fintype.sum_bijective Fintype.sum_bijective
 
-alias _root_.Function.Bijective.finset_prod := prod_bijective
-attribute [to_additive] Function.Bijective.finset_prod
+@[to_additive] alias _root_.Function.Bijective.finset_prod := prod_bijective
 
 /-- `Fintype.prod_equiv` is a specialization of `Finset.prod_bij` that
 automatically fills in most arguments.
@@ -2117,12 +2191,39 @@ See `Equiv.prod_comp` for a version without `h`.
 automatically fills in most arguments.
 
 See `Equiv.sum_comp` for a version without `h`."]
-theorem prod_equiv {α β M : Type*} [Fintype α] [Fintype β] [CommMonoid M] (e : α ≃ β) (f : α → M)
-    (g : β → M) (h : ∀ x, f x = g (e x)) : ∏ x : α, f x = ∏ x : β, g x :=
-  e.bijective.finset_prod _ f g h
+lemma prod_equiv (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ x, f x = g (e x)) :
+    ∏ x, f x = ∏ x, g x := prod_bijective _ e.bijective _ _ h
 #align fintype.prod_equiv Fintype.prod_equiv
 #align fintype.sum_equiv Fintype.sum_equiv
 
+@[to_additive]
+lemma _root_.Function.Bijective.prod_comp {e : ι → κ} (he : e.Bijective) (g : κ → α) :
+    ∏ i, g (e i) = ∏ i, g i := prod_bijective _ he _ _ fun _ ↦ rfl
+#align function.bijective.prod_comp Function.Bijective.prod_comp
+#align function.bijective.sum_comp Function.Bijective.sum_comp
+
+@[to_additive]
+lemma _root_.Equiv.prod_comp (e : ι ≃ κ) (g : κ → α) : ∏ i, g (e i) = ∏ i, g i :=
+  prod_equiv e _ _ fun _ ↦ rfl
+#align equiv.prod_comp Equiv.prod_comp
+#align equiv.sum_comp Equiv.sum_comp
+
+@[to_additive]
+lemma prod_fiberwise [DecidableEq κ] [Fintype ι] (g : ι → κ) (f : ι → α) :
+    ∏ j, ∏ i : {i // g i = j}, f i = ∏ i, f i := by
+  rw [← Finset.prod_fiberwise _ g f]
+  congr with j
+  exact (prod_subtype _ (by simp) _).symm
+#align fintype.prod_fiberwise Fintype.prod_fiberwise
+#align fintype.sum_fiberwise Fintype.sum_fiberwise
+
+@[to_additive]
+lemma prod_fiberwise' [DecidableEq κ] [Fintype ι] (g : ι → κ) (f : κ → α) :
+    ∏ j, ∏ _i : {i // g i = j}, f j = ∏ i, f (g i) := by
+  rw [← Finset.prod_fiberwise' _ g f]
+  congr with j
+  exact (prod_subtype _ (by simp) fun _ ↦ _).symm
+
 @[to_additive]
 theorem prod_unique {α β : Type*} [CommMonoid β] [Unique α] [Fintype α] (f : α → β) :
     ∏ x : α, f x = f default := by rw [univ_unique, prod_singleton]
@@ -2491,3 +2592,12 @@ theorem toAdd_prod (s : Finset ι) (f : ι → Multiplicative α) :
 #align to_add_prod toAdd_prod
 
 end AddCommMonoid
+
+/-!
+### Deprecated lemmas
+
+Those lemmas were deprecated on the 2023/12/23.
+-/
+
+@[deprecated] alias Equiv.prod_comp' := Fintype.prod_equiv
+@[deprecated] alias Equiv.sum_comp' := Fintype.sum_equiv
diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
index de4c32ff727b3..15d5f5e1c8fe2 100644
--- a/Mathlib/Algebra/BigOperators/Finprod.lean
+++ b/Mathlib/Algebra/BigOperators/Finprod.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 _
diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean
index 316ee175939b6..6abd5300cd09d 100644
--- a/Mathlib/Algebra/BigOperators/Finsupp.lean
+++ b/Mathlib/Algebra/BigOperators/Finsupp.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
diff --git a/Mathlib/Algebra/BigOperators/Intervals.lean b/Mathlib/Algebra/BigOperators/Intervals.lean
index f661f602e41d8..7568f0062b5df 100644
--- a/Mathlib/Algebra/BigOperators/Intervals.lean
+++ b/Mathlib/Algebra/BigOperators/Intervals.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' ⟨⟨_, _⟩, ⟨_, _⟩⟩ <;>
diff --git a/Mathlib/Algebra/BigOperators/Ring.lean b/Mathlib/Algebra/BigOperators/Ring.lean
index 8019d55d222ed..a49c66756c97f 100644
--- a/Mathlib/Algebra/BigOperators/Ring.lean
+++ b/Mathlib/Algebra/BigOperators/Ring.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)`. -/
diff --git a/Mathlib/Algebra/Tropical/BigOperators.lean b/Mathlib/Algebra/Tropical/BigOperators.lean
index 51b829e2861c8..738e54e3af19a 100644
--- a/Mathlib/Algebra/Tropical/BigOperators.lean
+++ b/Mathlib/Algebra/Tropical/BigOperators.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
diff --git a/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean b/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
index 47acaa261eed2..b84b183ea8ca6 100644
--- a/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
+++ b/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.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
 
 /-!
diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
index 8a8945c8e29a6..bdce464db1ce0 100644
--- a/Mathlib/Analysis/Analytic/Composition.lean
+++ b/Mathlib/Analysis/Analytic/Composition.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
diff --git a/Mathlib/Combinatorics/Configuration.lean b/Mathlib/Combinatorics/Configuration.lean
index b798e25edacf1..85825f46b961f 100644
--- a/Mathlib/Combinatorics/Configuration.lean
+++ b/Mathlib/Combinatorics/Configuration.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
diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
index 94daa0ee28250..22c0b65c9f658 100644
--- a/Mathlib/Data/Complex/Exponential.lean
+++ b/Mathlib/Data/Complex/Exponential.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
diff --git a/Mathlib/Data/DFinsupp/Basic.lean b/Mathlib/Data/DFinsupp/Basic.lean
index ab6ca2fbb9707..b7092d2244060 100644
--- a/Mathlib/Data/DFinsupp/Basic.lean
+++ b/Mathlib/Data/DFinsupp/Basic.lean
@@ -2151,9 +2151,8 @@ theorem sum_single [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable
 @[to_additive]
 theorem prod_subtypeDomain_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
     [CommMonoid γ] {v : Π₀ i, β i} {p : ι → Prop} [DecidablePred p] {h : ∀ i, β i → γ}
-    (hp : ∀ x ∈ v.support, p x) : ((v.subtypeDomain p).prod fun i b => h i b) = v.prod h :=
-  Finset.prod_bij (fun p _ => p) (by simp) (by simp) (fun ⟨a₀, ha₀⟩ ⟨a₁, ha₁⟩ => by simp)
-    fun i hi => ⟨⟨i, hp i hi⟩, by simpa using hi, rfl⟩
+    (hp : ∀ x ∈ v.support, p x) : (v.subtypeDomain p).prod (fun i b => h i b) = v.prod h := by
+  refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop
 #align dfinsupp.prod_subtype_domain_index DFinsupp.prod_subtypeDomain_index
 #align dfinsupp.sum_subtype_domain_index DFinsupp.sum_subtypeDomain_index
 
diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean
index 8a0629a17e43e..d25a8485d7820 100644
--- a/Mathlib/Data/Finset/Card.lean
+++ b/Mathlib/Data/Finset/Card.lean
@@ -399,14 +399,14 @@ theorem surj_on_of_inj_on_of_card_le {t : Finset β} (f : ∀ a ∈ s, β) (hf :
 #align finset.surj_on_of_inj_on_of_card_le Finset.surj_on_of_inj_on_of_card_le
 
 theorem inj_on_of_surj_on_of_card_le {t : Finset β} (f : ∀ a ∈ s, β) (hf : ∀ a ha, f a ha ∈ t)
-    (hsurj : ∀ b ∈ t, ∃ a ha, b = f a ha) (hst : s.card ≤ t.card) ⦃a₁ a₂⦄ (ha₁ : a₁ ∈ s)
+    (hsurj : ∀ b ∈ t, ∃ a ha, f a ha = b) (hst : s.card ≤ t.card) ⦃a₁⦄ (ha₁ : a₁ ∈ s) ⦃a₂⦄
     (ha₂ : a₂ ∈ s) (ha₁a₂ : f a₁ ha₁ = f a₂ ha₂) : a₁ = a₂ :=
   haveI : Inhabited { x // x ∈ s } := ⟨⟨a₁, ha₁⟩⟩
   let f' : { x // x ∈ s } → { x // x ∈ t } := fun x => ⟨f x.1 x.2, hf x.1 x.2⟩
   let g : { x // x ∈ t } → { x // x ∈ s } :=
     @surjInv _ _ f' fun x =>
       let ⟨y, hy₁, hy₂⟩ := hsurj x.1 x.2
-      ⟨⟨y, hy₁⟩, Subtype.eq hy₂.symm⟩
+      ⟨⟨y, hy₁⟩, Subtype.eq hy₂⟩
   have hg : Injective g := injective_surjInv _
   have hsg : Surjective g := fun x =>
     let ⟨y, hy⟩ :=
diff --git a/Mathlib/Data/Finset/LocallyFinite.lean b/Mathlib/Data/Finset/LocallyFinite.lean
index 9d9f6c0af93fe..700d0ac71ab4c 100644
--- a/Mathlib/Data/Finset/LocallyFinite.lean
+++ b/Mathlib/Data/Finset/LocallyFinite.lean
@@ -1179,7 +1179,7 @@ theorem prod_prod_Ioi_mul_eq_prod_prod_off_diag [Fintype ι] [LinearOrder ι]
   simp_rw [← Ioi_disjUnion_Iio, prod_disjUnion, prod_mul_distrib]
   congr 1
   rw [prod_sigma', prod_sigma']
-  refine' prod_bij' (fun i _ => ⟨i.2, i.1⟩) _ _ (fun i _ => ⟨i.2, i.1⟩) _ _ _ <;> simp
+  refine' prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) _ _ _ _ _ <;> simp
 #align finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag
 #align finset.sum_sum_Ioi_add_eq_sum_sum_off_diag Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag
 
diff --git a/Mathlib/Data/Finsupp/Antidiagonal.lean b/Mathlib/Data/Finsupp/Antidiagonal.lean
index 249a21f269ca9..36fcb225a2f10 100644
--- a/Mathlib/Data/Finsupp/Antidiagonal.lean
+++ b/Mathlib/Data/Finsupp/Antidiagonal.lean
@@ -56,9 +56,7 @@ theorem antidiagonal_zero : antidiagonal (0 : α →₀ ℕ) = singleton (0, 0)
 theorem prod_antidiagonal_swap {M : Type*} [CommMonoid M] (n : α →₀ ℕ)
     (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
     ∏ p in antidiagonal n, f p.1 p.2 = ∏ p in antidiagonal n, f p.2 p.1 :=
-  Finset.prod_bij (fun p _hp ↦ p.swap) (fun _p ↦ swap_mem_antidiagonal.2) (fun _p _hp ↦ rfl)
-    (fun _p₁ _p₂ _ _ h ↦ Prod.swap_injective h) fun p hp ↦
-    ⟨p.swap, swap_mem_antidiagonal.2 hp, p.swap_swap.symm⟩
+  prod_equiv (Equiv.prodComm _ _) (by simp [add_comm]) (by simp)
 #align finsupp.prod_antidiagonal_swap Finsupp.prod_antidiagonal_swap
 #align finsupp.sum_antidiagonal_swap Finsupp.sum_antidiagonal_swap
 
diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean
index 378919364cb2f..1032755daf26f 100644
--- a/Mathlib/Data/Finsupp/Basic.lean
+++ b/Mathlib/Data/Finsupp/Basic.lean
@@ -1052,9 +1052,8 @@ theorem subtypeDomain_eq_zero_iff {f : α →₀ M} (hf : ∀ x ∈ f.support, p
 
 @[to_additive]
 theorem prod_subtypeDomain_index [CommMonoid N] {v : α →₀ M} {h : α → M → N}
-    (hp : ∀ x ∈ v.support, p x) : ((v.subtypeDomain p).prod fun a b => h a b) = v.prod h :=
-  prod_bij (fun p _ => p.val) (fun _ => by classical exact mem_subtype.1) (fun _ _ => rfl)
-    (fun _ _ _ _ => Subtype.eq) fun b hb => ⟨⟨b, hp b hb⟩, by classical exact mem_subtype.2 hb, rfl⟩
+    (hp : ∀ x ∈ v.support, p x) : (v.subtypeDomain p).prod (fun a b ↦ h a b) = v.prod h := by
+  refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop
 #align finsupp.prod_subtype_domain_index Finsupp.prod_subtypeDomain_index
 #align finsupp.sum_subtype_domain_index Finsupp.sum_subtypeDomain_index
 
diff --git a/Mathlib/Data/Fintype/BigOperators.lean b/Mathlib/Data/Fintype/BigOperators.lean
index da93fd27a5c40..94cc552427eb2 100644
--- a/Mathlib/Data/Fintype/BigOperators.lean
+++ b/Mathlib/Data/Fintype/BigOperators.lean
@@ -173,13 +173,7 @@ theorem Finset.prod_attach_univ [Fintype α] [CommMonoid β] (f : { a : α // a
 theorem Finset.prod_univ_pi [DecidableEq α] [Fintype α] [CommMonoid β] {δ : α → Type*}
     {t : ∀ a : α, Finset (δ a)} (f : (∀ a : α, a ∈ (univ : Finset α) → δ a) → β) :
     ∏ x in univ.pi t, f x = ∏ x in Fintype.piFinset t, f fun a _ => x a := by
-  refine prod_bij (fun x _ a => x a (mem_univ _)) ?_ (by simp)
-    (by simp (config := { contextual := true }) [Function.funext_iff]) fun x hx =>
-    ⟨fun a _ => x a, by simp_all⟩
-  -- Porting note: old proof was `by simp`
-  intro a ha
-  simp only [Fintype.piFinset, mem_map, mem_pi, Function.Embedding.coeFn_mk]
-  exact ⟨a, by simpa using ha, by simp⟩
+  apply prod_nbij' (fun x i ↦ x i $ mem_univ _) (fun x i _ ↦ x i) <;> simp
 #align finset.prod_univ_pi Finset.prod_univ_pi
 #align finset.sum_univ_pi Finset.sum_univ_pi
 
@@ -202,34 +196,13 @@ theorem Fintype.sum_pow_mul_eq_add_pow (α : Type*) [Fintype α] {R : Type*} [Co
   Finset.sum_pow_mul_eq_add_pow _ _ _
 #align fintype.sum_pow_mul_eq_add_pow Fintype.sum_pow_mul_eq_add_pow
 
-@[to_additive]
-theorem Function.Bijective.prod_comp [Fintype α] [Fintype β] [CommMonoid γ] {f : α → β}
-    (hf : Function.Bijective f) (g : β → γ) : (∏ i, g (f i)) = ∏ i, g i :=
-  Fintype.prod_bijective f hf _ _ fun _x => rfl
-#align function.bijective.prod_comp Function.Bijective.prod_comp
-#align function.bijective.sum_comp Function.Bijective.sum_comp
-
-@[to_additive]
-theorem Equiv.prod_comp [Fintype α] [Fintype β] [CommMonoid γ] (e : α ≃ β) (f : β → γ) :
-    (∏ i, f (e i)) = ∏ i, f i :=
-  e.bijective.prod_comp f
-#align equiv.prod_comp Equiv.prod_comp
-#align equiv.sum_comp Equiv.sum_comp
-
-@[to_additive]
-theorem Equiv.prod_comp' [Fintype α] [Fintype β] [CommMonoid γ] (e : α ≃ β) (f : α → γ) (g : β → γ)
-    (h : ∀ i, f i = g (e i)) : ∏ i, f i = ∏ i, g i :=
-  (show f = g ∘ e from funext h).symm ▸ e.prod_comp _
-#align equiv.prod_comp' Equiv.prod_comp'
-#align equiv.sum_comp' Equiv.sum_comp'
-
 /-- It is equivalent to compute the product of a function over `Fin n` or `Finset.range n`. -/
 @[to_additive "It is equivalent to sum a function over `fin n` or `finset.range n`."]
 theorem Fin.prod_univ_eq_prod_range [CommMonoid α] (f : ℕ → α) (n : ℕ) :
     ∏ i : Fin n, f i = ∏ i in range n, f i :=
   calc
     ∏ i : Fin n, f i = ∏ i : { x // x ∈ range n }, f i :=
-      (Fin.equivSubtype.trans (Equiv.subtypeEquivRight (by simp))).prod_comp' _ _ (by simp)
+      Fintype.prod_equiv (Fin.equivSubtype.trans (Equiv.subtypeEquivRight (by simp))) _ _ (by simp)
     _ = ∏ i in range n, f i := by rw [← attach_eq_univ, prod_attach]
 #align fin.prod_univ_eq_prod_range Fin.prod_univ_eq_prod_range
 #align fin.sum_univ_eq_sum_range Fin.sum_univ_eq_sum_range
@@ -251,21 +224,6 @@ theorem Finset.prod_toFinset_eq_subtype {M : Type*} [CommMonoid M] [Fintype α]
 #align finset.prod_to_finset_eq_subtype Finset.prod_toFinset_eq_subtype
 #align finset.sum_to_finset_eq_subtype Finset.sum_toFinset_eq_subtype
 
-@[to_additive]
-theorem Finset.prod_fiberwise [DecidableEq β] [Fintype β] [CommMonoid γ] (s : Finset α) (f : α → β)
-    (g : α → γ) : (∏ b : β, ∏ a in s.filter fun a => f a = b, g a) = ∏ a in s, g a :=
-  Finset.prod_fiberwise_of_maps_to (fun _x _ => mem_univ _) _
-#align finset.prod_fiberwise Finset.prod_fiberwise
-#align finset.sum_fiberwise Finset.sum_fiberwise
-
-@[to_additive]
-theorem Fintype.prod_fiberwise [Fintype α] [DecidableEq β] [Fintype β] [CommMonoid γ] (f : α → β)
-    (g : α → γ) : (∏ b : β, ∏ a : { a // f a = b }, g (a : α)) = ∏ a, g a := by
-  rw [← (Equiv.sigmaFiberEquiv f).prod_comp, ← univ_sigma_univ, prod_sigma]
-  rfl
-#align fintype.prod_fiberwise Fintype.prod_fiberwise
-#align fintype.sum_fiberwise Fintype.sum_fiberwise
-
 nonrec theorem Fintype.prod_dite [Fintype α] {p : α → Prop} [DecidablePred p] [CommMonoid β]
     (f : ∀ a, p a → β) (g : ∀ a, ¬p a → β) :
     (∏ a, dite (p a) (f a) (g a)) =
diff --git a/Mathlib/Data/Multiset/Nodup.lean b/Mathlib/Data/Multiset/Nodup.lean
index d1418b4021db3..1a27d4e730c1e 100644
--- a/Mathlib/Data/Multiset/Nodup.lean
+++ b/Mathlib/Data/Multiset/Nodup.lean
@@ -167,6 +167,8 @@ theorem nodup_attach {s : Multiset α} : Nodup (attach s) ↔ Nodup s :=
   Quot.induction_on s fun _ => List.nodup_attach
 #align multiset.nodup_attach Multiset.nodup_attach
 
+protected alias ⟨_, Nodup.attach⟩ := nodup_attach
+
 theorem Nodup.pmap {p : α → Prop} {f : ∀ a, p a → β} {s : Multiset α} {H}
     (hf : ∀ a ha b hb, f a ha = f b hb → a = b) : Nodup s → Nodup (pmap f s H) :=
   Quot.induction_on s (fun _ _ => List.Nodup.pmap hf) H
@@ -265,16 +267,12 @@ theorem mem_sub_of_nodup [DecidableEq α] {a : α} {s t : Multiset α} (d : Nodu
 
 theorem map_eq_map_of_bij_of_nodup (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β}
     (hs : s.Nodup) (ht : t.Nodup) (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t)
-    (h : ∀ a ha, f a = g (i a ha)) (i_inj : ∀ a₁ a₂ ha₁ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
-    (i_surj : ∀ b ∈ t, ∃ a ha, b = i a ha) : s.map f = t.map g :=
-  have : t = s.attach.map fun x => i x.1 x.2 :=
-    (ht.ext <|
-          (nodup_attach.2 hs).map <|
-            show Injective fun x : { x // x ∈ s } => i x x.2 from fun x y hxy =>
-              Subtype.ext <| i_inj x y x.2 y.2 hxy).2
-      fun x => by
-        simp only [mem_map, true_and_iff, Subtype.exists, eq_comm, mem_attach]
-        exact ⟨i_surj _, fun ⟨y, hy⟩ => hy.snd.symm ▸ hi _ _⟩
+    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
+    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) : s.map f = t.map g := by
+  have : t = s.attach.map fun x => i x.1 x.2
+  · rw [ht.ext]
+    · aesop
+    · exact hs.attach.map $ fun x y hxy ↦ Subtype.ext $ i_inj _ x.2 _ y.2 hxy
   calc
     s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
     _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
diff --git a/Mathlib/Data/Polynomial/Mirror.lean b/Mathlib/Data/Polynomial/Mirror.lean
index 862bc472591db..83763fc7ba080 100644
--- a/Mathlib/Data/Polynomial/Mirror.lean
+++ b/Mathlib/Data/Polynomial/Mirror.lean
@@ -107,10 +107,10 @@ theorem mirror_eval_one : p.mirror.eval 1 = p.eval 1 := by
     rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
     rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]
     exact natTrailingDegree_le_of_ne_zero hp
-  · exact fun n₁ n₂ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]
+  · exact fun n₁ _ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]
   · intro n hn hp
     use revAt (p.natDegree + p.natTrailingDegree) n
-    refine' ⟨_, _, revAt_invol.symm⟩
+    refine' ⟨_, _, revAt_invol⟩
     · rw [Finset.mem_range_succ_iff] at *
       rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
       rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]
diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index dc3eb508ede59..a3fc6cd9b5346 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -804,7 +804,7 @@ theorem surj_on_of_inj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : 
 #align set.surj_on_of_inj_on_of_ncard_le Set.surj_on_of_inj_on_of_ncard_le
 
 theorem inj_on_of_surj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : ∀ a ha, f a ha ∈ t)
-    (hsurj : ∀ b ∈ t, ∃ a ha, b = f a ha) (hst : s.ncard ≤ t.ncard) ⦃a₁ a₂⦄ (ha₁ : a₁ ∈ s)
+    (hsurj : ∀ b ∈ t, ∃ a ha, f a ha = b) (hst : s.ncard ≤ t.ncard) ⦃a₁⦄ (ha₁ : a₁ ∈ s) ⦃a₂⦄
     (ha₂ : a₂ ∈ s) (ha₁a₂ : f a₁ ha₁ = f a₂ ha₂) (hs : s.Finite := by toFinite_tac) :
     a₁ = a₂ := by
   classical
@@ -820,8 +820,8 @@ theorem inj_on_of_surj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : 
   exact
     @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
       (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
-      (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁ a₂
-      (by simpa) (by simpa) (by simpa)
+      (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
+      (by simpa) a₂ (by simpa) (by simpa)
 #align set.inj_on_of_surj_on_of_ncard_le Set.inj_on_of_surj_on_of_ncard_le
 
 section Lattice
diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
index 14fd58c7716c1..77bbdac706897 100644
--- a/Mathlib/Data/Set/Finite.lean
+++ b/Mathlib/Data/Set/Finite.lean
@@ -892,7 +892,7 @@ lemma Finite.of_surjOn {s : Set α} {t : Set β} (f : α → β) (hf : SurjOn f
     t.Finite := (hs.image _).subset hf
 
 theorem Finite.dependent_image {s : Set α} (hs : s.Finite) (F : ∀ i ∈ s, β) :
-    { y : β | ∃ (x : _) (hx : x ∈ s), y = F x hx }.Finite := by
+    {y : β | ∃ x hx, F x hx = y}.Finite := by
   cases hs
   simpa [range, eq_comm] using finite_range fun x : s => F x x.2
 #align set.finite.dependent_image Set.Finite.dependent_image
diff --git a/Mathlib/Data/Sign.lean b/Mathlib/Data/Sign.lean
index 0954d3a48353d..34aff1961e3ce 100644
--- a/Mathlib/Data/Sign.lean
+++ b/Mathlib/Data/Sign.lean
@@ -518,7 +518,7 @@ theorem exists_signed_sum {α : Type u_1} [DecidableEq α] (s : Finset α) (f :
           ∀ a ∈ s, (∑ b, if g b = a then (sgn b : ℤ) else 0) = f a :=
   let ⟨β, t, sgn, g, hg, ht, hf⟩ := exists_signed_sum_aux s f
   ⟨t, inferInstance, fun b => sgn b, fun b => g b, fun b => hg b, by simp [ht], fun a ha =>
-    (@sum_attach _ _ t _ fun b => ite (g b = a) (sgn b : ℤ) 0).trans <| hf _ ha⟩
+    (sum_attach t fun b ↦ ite (g b = a) (sgn b : ℤ) 0).trans <| hf _ ha⟩
 #align exists_signed_sum exists_signed_sum
 
 /-- We can decompose a sum of absolute value less than `n` into a sum of at most `n` signs. -/
diff --git a/Mathlib/FieldTheory/Fixed.lean b/Mathlib/FieldTheory/Fixed.lean
index 7665979fd3d83..cb2d229512be5 100644
--- a/Mathlib/FieldTheory/Fixed.lean
+++ b/Mathlib/FieldTheory/Fixed.lean
@@ -144,7 +144,7 @@ theorem linearIndependent_smul_of_linearIndependent {s : Finset F} :
       (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) _ ⟨i, his⟩
           (mem_attach _ _) :
         _)
-  refine' (@sum_attach _ _ s _ fun i => (g • l i - l i) • MulAction.toFun G F i).trans _
+  refine' (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans _
   ext g'; dsimp only
   conv_lhs =>
     rw [sum_apply]
diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean
index 261210b0e8032..6ccc3e3b556f8 100644
--- a/Mathlib/GroupTheory/PGroup.lean
+++ b/Mathlib/GroupTheory/PGroup.lean
@@ -199,7 +199,7 @@ theorem card_modEq_card_fixedPoints [Fintype (fixedPoints G α)] :
     refine'
       Eq.symm
         (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
-          (fun a₁ a₂ _ _ _ _ h =>
+          (fun a₁ _ _ a₂ _ _ h =>
             Subtype.eq (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
           (fun b => Quotient.inductionOn' b fun b _ hb => _) fun a ha _ => by
           rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean
index 5d00783df7b7a..3c26db827af4c 100644
--- a/Mathlib/GroupTheory/Perm/Sign.lean
+++ b/Mathlib/GroupTheory/Perm/Sign.lean
@@ -328,21 +328,20 @@ def signBijAux {n : ℕ} (f : Perm (Fin n)) (a : Σ_ : Fin n, Fin n) : Σ_ : Fin
 
 -- porting note: Lean insists `ha` and `hb` are unused despite obvious uses
 set_option linter.unusedVariables false in
-theorem signBijAux_inj {n : ℕ} {f : Perm (Fin n)} :
-    ∀ a b : Σ_a : Fin n, Fin n,
-      a ∈ finPairsLT n → b ∈ finPairsLT n → signBijAux f a = signBijAux f b → a = b :=
-  fun ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h => by
-    unfold signBijAux at h
-    rw [mem_finPairsLT] at *
-    have : ¬b₁ < b₂ := hb.le.not_lt
-    split_ifs at h <;>
-    simp_all [(Equiv.injective f).eq_iff, eq_self_iff_true, and_self_iff, heq_iff_eq]
-    · exact absurd this (not_le.mpr ha)
-    · exact absurd this (not_le.mpr ha)
-#align equiv.perm.sign_bij_aux_inj Equiv.Perm.signBijAux_inj
+theorem signBijAux_injOn {n : ℕ} {f : Perm (Fin n)} :
+    (finPairsLT n : Set (Σ _, Fin n)).InjOn (signBijAux f) := by
+  rintro ⟨a₁, a₂⟩ ha ⟨b₁, b₂⟩ hb h
+  dsimp [signBijAux] at h
+  rw [Finset.mem_coe, mem_finPairsLT] at *
+  have : ¬b₁ < b₂ := hb.le.not_lt
+  split_ifs at h <;>
+  simp_all [(Equiv.injective f).eq_iff, eq_self_iff_true, and_self_iff, heq_iff_eq]
+  · exact absurd this (not_le.mpr ha)
+  · exact absurd this (not_le.mpr ha)
+#align equiv.perm.sign_bij_aux_inj Equiv.Perm.signBijAux_injOn
 
 theorem signBijAux_surj {n : ℕ} {f : Perm (Fin n)} :
-    ∀ a ∈ finPairsLT n, ∃ (b: Σ (_: Fin n), Fin n) (_H: b ∈ finPairsLT n), a = signBijAux f b :=
+    ∀ a ∈ finPairsLT n, ∃ b ∈ finPairsLT n, signBijAux f b = a :=
   fun ⟨a₁, a₂⟩ ha =>
     if hxa : f⁻¹ a₂ < f⁻¹ a₁ then
       ⟨⟨f⁻¹ a₁, f⁻¹ a₂⟩, mem_finPairsLT.2 hxa, by
@@ -369,41 +368,37 @@ theorem signBijAux_mem {n : ℕ} {f : Perm (Fin n)} :
 
 @[simp]
 theorem signAux_inv {n : ℕ} (f : Perm (Fin n)) : signAux f⁻¹ = signAux f :=
-  prod_bij (fun a _ => signBijAux f⁻¹ a) signBijAux_mem
-    (fun ⟨a, b⟩ hab =>
-      if h : f⁻¹ b < f⁻¹ a then by
-        simp_all [signBijAux, dif_pos h, if_neg h.not_le, apply_inv_self, apply_inv_self,
-          if_neg (mem_finPairsLT.1 hab).not_le]
-        split_ifs with h₁
-        · dsimp [finPairsLT] at hab
-          simp? at hab says
-            simp only [mem_sigma, mem_univ, mem_attachFin, mem_range, Fin.val_fin_lt,
-              true_and] at hab
-          exact absurd h₁ (not_le_of_gt hab)
-        · rfl
-      else by
-        simp_all [signBijAux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self, apply_inv_self,
-          if_pos (mem_finPairsLT.1 hab).le]
-        split_ifs with h₁ h₂ h₃
-        · rfl
-        · exact absurd h (not_le_of_gt h₁)
-        · rfl
-        · dsimp at *
-          dsimp [finPairsLT] at hab
-          simp? at * says
-            simp only [mem_sigma, mem_univ, mem_attachFin, mem_range, Fin.val_fin_lt,
-              true_and, not_lt, apply_inv_self, not_le, Int.neg_units_ne_self] at *
-          exact absurd h₃ (asymm_of LT.lt hab))
-    signBijAux_inj signBijAux_surj
+  prod_nbij (signBijAux f⁻¹) signBijAux_mem signBijAux_injOn signBijAux_surj fun ⟨a, b⟩ hab ↦
+    if h : f⁻¹ b < f⁻¹ a then by
+      simp_all [signBijAux, dif_pos h, if_neg h.not_le, apply_inv_self, apply_inv_self,
+        if_neg (mem_finPairsLT.1 hab).not_le]
+      split_ifs with h₁
+      · dsimp [finPairsLT] at hab
+        simp? at hab says
+          simp only [mem_sigma, mem_univ, mem_attachFin, mem_range, Fin.val_fin_lt,
+            true_and] at hab
+        exact absurd h₁ (not_le_of_gt hab)
+      · rfl
+    else by
+      simp_all [signBijAux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self, apply_inv_self,
+        if_pos (mem_finPairsLT.1 hab).le]
+      split_ifs with h₁ h₂ h₃
+      · rfl
+      · exact absurd h (not_le_of_gt h₁)
+      · rfl
+      · dsimp at *
+        dsimp [finPairsLT] at hab
+        simp? at * says
+          simp only [mem_sigma, mem_univ, mem_attachFin, mem_range, Fin.val_fin_lt,
+            true_and, not_lt, apply_inv_self, not_le, Int.neg_units_ne_self] at *
+        exact absurd h₃ (asymm_of LT.lt hab)
 #align equiv.perm.sign_aux_inv Equiv.Perm.signAux_inv
 
 theorem signAux_mul {n : ℕ} (f g : Perm (Fin n)) : signAux (f * g) = signAux f * signAux g := by
   rw [← signAux_inv g]
   unfold signAux
   rw [← prod_mul_distrib]
-  refine'
-    prod_bij (fun a _ => signBijAux g a) signBijAux_mem _ signBijAux_inj
-    (by simpa using signBijAux_surj)
+  refine prod_nbij (signBijAux g) signBijAux_mem signBijAux_injOn signBijAux_surj ?_
   rintro ⟨a, b⟩ hab
   dsimp only [signBijAux]
   rw [mul_apply, mul_apply]
diff --git a/Mathlib/GroupTheory/SchurZassenhaus.lean b/Mathlib/GroupTheory/SchurZassenhaus.lean
index 30095bd8c7498..c781a463b753f 100644
--- a/Mathlib/GroupTheory/SchurZassenhaus.lean
+++ b/Mathlib/GroupTheory/SchurZassenhaus.lean
@@ -59,14 +59,9 @@ theorem smul_diff_smul' [hH : Normal H] (g : Gᵐᵒᵖ) :
       map_one' := by rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_self]
       map_mul' := fun h₁ h₂ => by
         simp only [Subtype.ext_iff, coe_mk, coe_mul, mul_assoc, mul_inv_cancel_left] }
-  refine'
-    Eq.trans
-      (Finset.prod_bij' (fun q _ => g⁻¹ • q) (fun q _ => Finset.mem_univ _)
-        (fun q _ => Subtype.ext _) (fun q _ => g • q) (fun q _ => Finset.mem_univ _)
-        (fun q _ => smul_inv_smul g q) fun q _ => inv_smul_smul g q)
-      (map_prod ϕ _ _).symm
-  simp only [MonoidHom.id_apply, MonoidHom.coe_mk, OneHom.coe_mk,
-    smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc]
+  refine (Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm
+  simp only [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc,
+    MonoidHom.id_apply, toPerm_symm_apply, MonoidHom.coe_mk, OneHom.coe_mk]
 #align subgroup.smul_diff_smul' Subgroup.smul_diff_smul'
 
 variable {H} [Normal H]
diff --git a/Mathlib/GroupTheory/Transfer.lean b/Mathlib/GroupTheory/Transfer.lean
index abe4c606c8b7f..40e81534d69a2 100644
--- a/Mathlib/GroupTheory/Transfer.lean
+++ b/Mathlib/GroupTheory/Transfer.lean
@@ -79,14 +79,9 @@ theorem diff_inv : (diff ϕ S T)⁻¹ = diff ϕ T S :=
 @[to_additive]
 theorem smul_diff_smul (g : G) : diff ϕ (g • S) (g • T) = diff ϕ S T :=
   let _ := H.fintypeQuotientOfFiniteIndex
-  prod_bij' (fun q _ => g⁻¹ • q) (fun _ _ => mem_univ _)
-    (fun _ _ =>
-      congr_arg ϕ
-        (by
-          simp_rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc,
-            inv_mul_cancel_left]))
-    (fun q _ => g • q) (fun _ _ => mem_univ _) (fun q _ => smul_inv_smul g q) fun q _ =>
-    inv_smul_smul g q
+  Fintype.prod_equiv (MulAction.toPerm g).symm _ _ $ fun _ ↦ by
+    simp only [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc,
+      inv_mul_cancel_left, toPerm_symm_apply]
 #align subgroup.left_transversals.smul_diff_smul Subgroup.leftTransversals.smul_diff_smul
 #align add_subgroup.left_transversals.vadd_diff_vadd AddSubgroup.leftTransversals.vadd_diff_vadd
 
diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant.lean b/Mathlib/LinearAlgebra/Matrix/Determinant.lean
index 927d256e85f6e..30018656a2541 100644
--- a/Mathlib/LinearAlgebra/Matrix/Determinant.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Determinant.lean
@@ -160,9 +160,9 @@ theorem det_mul (M N : Matrix n n R) : det (M * N) = det M * det N :=
         sum_subset (filter_subset _ _) fun f _ hbij =>
           det_mul_aux <| by simpa only [true_and_iff, mem_filter, mem_univ] using hbij)
     _ = ∑ τ : Perm n, ∑ σ : Perm n, ε σ * ∏ i, M (σ i) (τ i) * N (τ i) i :=
-      (sum_bij (fun p h => Equiv.ofBijective p (mem_filter.1 h).2) (fun _ _ => mem_univ _)
-        (fun _ _ => rfl) (fun _ _ _ _ h => by injection h) fun b _ =>
-        ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, coe_fn_injective rfl⟩)
+      sum_bij (fun p h ↦ Equiv.ofBijective p (mem_filter.1 h).2) (fun _ _ ↦ mem_univ _)
+        (fun _ _ _ _ h ↦ by injection h)
+        (fun b _ ↦ ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, coe_fn_injective rfl⟩) fun _ _ ↦ rfl
     _ = ∑ σ : Perm n, ∑ τ : Perm n, (∏ i, N (σ i) i) * ε τ * ∏ j, M (τ j) (σ j) := by
       simp only [mul_comm, mul_left_comm, prod_mul_distrib, mul_assoc]
     _ = ∑ σ : Perm n, ∑ τ : Perm n, (∏ i, N (σ i) i) * (ε σ * ε τ) * ∏ i, M (τ i) i :=
@@ -585,19 +585,12 @@ theorem det_blockDiagonal {o : Type*} [Fintype o] [DecidableEq o] (M : o → Mat
     Finset.mem_filter.trans ⟨fun h => h.2, fun h => ⟨Finset.mem_univ _, h⟩⟩
   rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _]
   -- And that these are in bijection with `o → Equiv.Perm m`.
-  rw [(Finset.sum_bij
-        (fun (σ : ∀ k : o, k ∈ Finset.univ → Equiv.Perm n) _ =>
-          prodCongrLeft fun k => σ k (Finset.mem_univ k))
-        _ _ _ _).symm]
+  refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).symm
   · intro σ _
     rw [mem_preserving_snd]
     rintro ⟨-, x⟩
     simp only [prodCongrLeft_apply]
-  · intro σ _
-    rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right]
-    simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq,
-      prodCongrLeft_apply]
-  · intro σ σ' _ _ eq
+  · intro σ _ σ' _ eq
     ext x hx k
     simp only at eq
     have :
@@ -632,6 +625,10 @@ theorem det_blockDiagonal {o : Type*} [Fintype o] [DecidableEq o] (M : o → Mat
     · ext ⟨k, x⟩
       · simp only [coe_fn_mk, prodCongrLeft_apply]
       · simp only [prodCongrLeft_apply, hσ]
+  · intro σ _
+    rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right]
+    simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq,
+      prodCongrLeft_apply]
   · intro σ _ hσ
     rw [mem_preserving_snd] at hσ
     obtain ⟨⟨k, x⟩, hkx⟩ := not_forall.mp hσ
@@ -652,21 +649,13 @@ theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Mat
       sum_subset (β := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (Sum m n))).toFinset) ?_
     rw [sum_mul_sum]
     simp_rw [univ_product_univ]
-    rw [(sum_bij (fun (σ : Perm m × Perm n) _ => Equiv.sumCongr σ.fst σ.snd) _ _ _ _).symm]
-    · intro σ₁₂ h
+    refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
+    · intro σ₁₂ _
       simp only
       erw [Set.mem_toFinset, MonoidHom.mem_range]
       use σ₁₂
       simp only [sumCongrHom_apply]
-    · simp only [forall_prop_of_true, Prod.forall, mem_univ]
-      intro σ₁ σ₂
-      rw [Fintype.prod_sum_type]
-      simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
-        fromBlocks_apply₂₂]
-      rw [mul_mul_mul_comm]
-      congr
-      rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
-    · intro σ₁ σ₂ h₁ h₂
+    · intro σ₁ _ σ₂ _
       dsimp only
       intro h
       have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
@@ -682,6 +671,14 @@ theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Mat
       use σ₁₂
       rw [← hσ₁₂]
       simp
+    · simp only [forall_prop_of_true, Prod.forall, mem_univ]
+      intro σ₁ σ₂
+      rw [Fintype.prod_sum_type]
+      simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
+        fromBlocks_apply₂₂]
+      rw [mul_mul_mul_comm]
+      congr
+      rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
     · rintro σ - hσn
       have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by
         rw [Set.mem_toFinset] at hσn
diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
index 06a39f065e3eb..e367c821630d4 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -302,35 +302,8 @@ theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) :
     (f * g) • h = f • g • h := by
   ext n
   simp only [mul_apply, smul_apply, sum_smul, mul_smul, smul_sum, Finset.sum_sigma']
-  apply Finset.sum_bij
-  pick_goal 5
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ _H
-    exact ⟨(k, l * j), (l, j)⟩
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ H
-    simp only [Finset.mem_sigma, mem_divisorsAntidiagonal] at H ⊢
-    rcases H with ⟨⟨rfl, n0⟩, rfl, i0⟩
-    refine' ⟨⟨(mul_assoc _ _ _).symm, n0⟩, trivial, _⟩
-    rw [mul_ne_zero_iff] at *
-    exact ⟨i0.2, n0.2⟩
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ _H
-    simp only [mul_assoc]
-  · rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩ ⟨⟨i, j⟩, ⟨k, l⟩⟩ H₁ H₂
-    simp only [Finset.mem_sigma, mem_divisorsAntidiagonal, and_imp, Prod.mk.inj_iff, add_comm,
-      heq_iff_eq] at H₁ H₂ ⊢
-    simp only [Sigma.mk.inj_iff, Prod.mk.injEq, heq_eq_eq, and_imp] -- porting note: added
-    rintro h h2 rfl rfl
-    subst h -- porting note: added.  The `rintro h ...` above was `rintro rfl ...`
-    exact ⟨⟨Eq.trans H₁.2.1.symm H₂.2.1, rfl⟩, rfl, rfl⟩
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ H
-    refine' ⟨⟨(i * k, l), (i, k)⟩, _, _⟩
-    · simp only [Finset.mem_sigma, mem_divisorsAntidiagonal] at H ⊢
-      rcases H with ⟨⟨rfl, n0⟩, rfl, j0⟩
-      refine' ⟨⟨mul_assoc _ _ _, n0⟩, trivial, _⟩
-      rw [mul_ne_zero_iff] at *
-      exact ⟨n0.1, j0.1⟩
-    · simp only [true_and_iff, mem_divisorsAntidiagonal, and_true_iff, Prod.mk.inj_iff,
-        eq_self_iff_true, Ne.def, mem_sigma, heq_iff_eq] at H ⊢
-      rw [H.2.1]
+  apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩)
+    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩) <;> aesop (add simp mul_assoc)
 #align nat.arithmetic_function.mul_smul' Nat.ArithmeticFunction.mul_smul'
 
 theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by
@@ -638,69 +611,64 @@ theorem int_cast {f : ArithmeticFunction ℤ} [Ring R] (h : f.IsMultiplicative)
 #align nat.arithmetic_function.is_multiplicative.int_cast Nat.ArithmeticFunction.IsMultiplicative.int_cast
 
 theorem mul [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative)
-    (hg : g.IsMultiplicative) : IsMultiplicative (f * g) :=
-  ⟨by
-    -- porting note was `simp [hf, hg]`.
-    simp [hf.1, hg.1],
-  by
-    simp only [mul_apply]
-    intro m n cop
-    rw [sum_mul_sum]
-    symm
-    apply sum_bij fun (x : (ℕ × ℕ) × ℕ × ℕ) _h => (x.1.1 * x.2.1, x.1.2 * x.2.2)
-    · rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h
-      simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h
-      rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
-      simp only [mem_divisorsAntidiagonal, Nat.mul_eq_zero, Ne.def]
-      constructor
-      · ring
-      rw [Nat.mul_eq_zero] at *
-      apply not_or_of_not ha hb
-    · rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h
-      simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h
-      rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
-      dsimp only
-      rw [hf.map_mul_of_coprime cop.coprime_mul_right.coprime_mul_right_right,
-        hg.map_mul_of_coprime cop.coprime_mul_left.coprime_mul_left_right]
-      ring
-    · rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ ⟨⟨c1, c2⟩, ⟨d1, d2⟩⟩ hab hcd h
-      simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at hab
-      rcases hab with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
-      simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at hcd
-      simp only [Prod.mk.inj_iff] at h
-      ext <;> dsimp only
-      · trans Nat.gcd (a1 * a2) (a1 * b1)
-        · rw [Nat.gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
-        · rw [← hcd.1.1, ← hcd.2.1] at cop
-          rw [← hcd.1.1, h.1, Nat.gcd_mul_left,
-            cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
-      · trans Nat.gcd (a1 * a2) (a2 * b2)
-        · rw [mul_comm, Nat.gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
-            mul_one]
-        · rw [← hcd.1.1, ← hcd.2.1] at cop
-          rw [← hcd.1.1, h.2, mul_comm, Nat.gcd_mul_left,
-            cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one, mul_one]
-      · trans Nat.gcd (b1 * b2) (a1 * b1)
-        · rw [mul_comm, Nat.gcd_mul_right,
-            cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, one_mul]
-        · rw [← hcd.1.1, ← hcd.2.1] at cop
-          rw [← hcd.2.1, h.1, mul_comm c1 d1, Nat.gcd_mul_left,
-            cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, mul_one]
-      · trans Nat.gcd (b1 * b2) (a2 * b2)
-        · rw [Nat.gcd_mul_right, cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one,
-            one_mul]
-        · rw [← hcd.1.1, ← hcd.2.1] at cop
-          rw [← hcd.2.1, h.2, Nat.gcd_mul_right,
-            cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]
-    · rintro ⟨b1, b2⟩ h
-      simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h
-      use ((b1.gcd m, b2.gcd m), (b1.gcd n, b2.gcd n))
-      simp only [exists_prop, Prod.mk.inj_iff, Ne.def, mem_product, mem_divisorsAntidiagonal]
-      rw [← cop.gcd_mul _, ← cop.gcd_mul _, ← h.1, Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul cop h.1,
-        Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul cop.symm _]
-      · rw [Nat.mul_eq_zero, not_or] at h
-        simp [h.2.1, h.2.2]
-      rw [mul_comm n m, h.1]⟩
+    (hg : g.IsMultiplicative) : IsMultiplicative (f * g) := by
+  refine ⟨by simp [hf.1, hg.1], ?_⟩
+  simp only [mul_apply]
+  intro m n cop
+  rw [sum_mul_sum]
+  symm
+  apply sum_nbij fun ((i, j), k, l) ↦ (i * k, j * l)
+  · rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h
+    simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h
+    rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
+    simp only [mem_divisorsAntidiagonal, Nat.mul_eq_zero, Ne.def]
+    constructor
+    · ring
+    rw [Nat.mul_eq_zero] at *
+    apply not_or_of_not ha hb
+  · simp only [Set.InjOn, mem_coe, mem_divisorsAntidiagonal, Ne.def, mem_product, Prod.mk.inj_iff]
+    rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩ ⟨⟨c1, c2⟩, ⟨d1, d2⟩⟩ hcd h
+    simp only [Prod.mk.inj_iff] at h
+    ext <;> dsimp only
+    · trans Nat.gcd (a1 * a2) (a1 * b1)
+      · rw [Nat.gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
+      · rw [← hcd.1.1, ← hcd.2.1] at cop
+        rw [← hcd.1.1, h.1, Nat.gcd_mul_left,
+          cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
+    · trans Nat.gcd (a1 * a2) (a2 * b2)
+      · rw [mul_comm, Nat.gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
+          mul_one]
+      · rw [← hcd.1.1, ← hcd.2.1] at cop
+        rw [← hcd.1.1, h.2, mul_comm, Nat.gcd_mul_left,
+          cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one, mul_one]
+    · trans Nat.gcd (b1 * b2) (a1 * b1)
+      · rw [mul_comm, Nat.gcd_mul_right,
+          cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, one_mul]
+      · rw [← hcd.1.1, ← hcd.2.1] at cop
+        rw [← hcd.2.1, h.1, mul_comm c1 d1, Nat.gcd_mul_left,
+          cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, mul_one]
+    · trans Nat.gcd (b1 * b2) (a2 * b2)
+      · rw [Nat.gcd_mul_right, cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one,
+          one_mul]
+      · rw [← hcd.1.1, ← hcd.2.1] at cop
+        rw [← hcd.2.1, h.2, Nat.gcd_mul_right,
+          cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]
+  · simp only [Set.SurjOn, Set.subset_def, mem_coe, mem_divisorsAntidiagonal, Ne.def, mem_product,
+      Set.mem_image, exists_prop, Prod.mk.inj_iff]
+    rintro ⟨b1, b2⟩ h
+    dsimp at h
+    use ((b1.gcd m, b2.gcd m), (b1.gcd n, b2.gcd n))
+    rw [← cop.gcd_mul _, ← cop.gcd_mul _, ← h.1, Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul cop h.1,
+      Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul cop.symm _]
+    · rw [Nat.mul_eq_zero, not_or] at h
+      simp [h.2.1, h.2.2]
+    rw [mul_comm n m, h.1]
+  · simp only [mem_divisorsAntidiagonal, Ne.def, mem_product]
+    rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
+    dsimp only
+    rw [hf.map_mul_of_coprime cop.coprime_mul_right.coprime_mul_right_right,
+      hg.map_mul_of_coprime cop.coprime_mul_left.coprime_mul_left_right]
+    ring
 #align nat.arithmetic_function.is_multiplicative.mul Nat.ArithmeticFunction.IsMultiplicative.mul
 
 theorem pmul [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative)
diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
index bc74b965696b2..f672a452c7d8e 100644
--- a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
+++ b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
@@ -41,7 +41,7 @@ theorem Ico_map_valMinAbs_natAbs_eq_Ico_map_id (p : ℕ) [hp : Fact p.Prime] (a
     simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, lt_succ_iff, succ_le_iff, pos_iff_ne_zero,
       natAbs_valMinAbs_le _]
   have hsurj : ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ),
-      ∃ x ∈ Ico 1 (p / 2).succ, b = (a * x : ZMod p).valMinAbs.natAbs := by
+      ∃ x, ∃ _ : x ∈ Ico 1 (p / 2).succ, (a * x : ZMod p).valMinAbs.natAbs = b := by
     intro b hb
     refine' ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨_, _⟩, _⟩
     · apply Nat.pos_of_ne_zero
@@ -54,10 +54,9 @@ theorem Ico_map_valMinAbs_natAbs_eq_Ico_map_id (p : ℕ) [hp : Fact p.Prime] (a
           if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_ofNat]
       · erw [mul_neg, mul_div_cancel' _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
           val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_ofNat]
-  simp only [← exists_prop] at hsurj
   exact Multiset.map_eq_map_of_bij_of_nodup _ _ (Finset.nodup _) (Finset.nodup _)
-    (fun x _ => (a * x : ZMod p).valMinAbs.natAbs) hmem (fun _ _ => rfl)
-    (inj_on_of_surj_on_of_card_le _ hmem hsurj le_rfl) hsurj
+    (fun x _ => (a * x : ZMod p).valMinAbs.natAbs) hmem
+    (inj_on_of_surj_on_of_card_le _ hmem hsurj le_rfl) hsurj (fun _ _ => rfl)
 #align zmod.Ico_map_val_min_abs_nat_abs_eq_Ico_map_id ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id
 
 private theorem gauss_lemma_aux₁ (p : ℕ) [Fact p.Prime] {a : ℤ}
diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean
index 2e567a148a1cd..31a85ba3acf4b 100644
--- a/Mathlib/NumberTheory/NumberField/Embeddings.lean
+++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean
@@ -511,7 +511,7 @@ open scoped BigOperators
 theorem prod_eq_abs_norm (x : K) :
     ∏ w : InfinitePlace K, w x ^ mult w = abs (Algebra.norm ℚ x) := by
   convert (congr_arg Complex.abs (@Algebra.norm_eq_prod_embeddings ℚ _ _ _ _ ℂ _ _ _ _ _ x)).symm
-  · rw [map_prod, ← Equiv.prod_comp' RingHom.equivRatAlgHom (fun f => Complex.abs (f x))
+  · rw [map_prod, ← Fintype.prod_equiv RingHom.equivRatAlgHom (fun f => Complex.abs (f x))
       (fun φ => Complex.abs (φ x)) fun _ => by simp [RingHom.equivRatAlgHom_apply]; rfl]
     rw [← Finset.prod_fiberwise Finset.univ (fun φ => mk φ) (fun φ => Complex.abs (φ x))]
     have : ∀ w : InfinitePlace K, ∀ φ ∈ Finset.filter (fun a ↦ mk a = w) Finset.univ,
diff --git a/Mathlib/NumberTheory/Wilson.lean b/Mathlib/NumberTheory/Wilson.lean
index 719004dc51467..79878b7a5c86b 100644
--- a/Mathlib/NumberTheory/Wilson.lean
+++ b/Mathlib/NumberTheory/Wilson.lean
@@ -59,7 +59,6 @@ theorem wilsons_lemma : ((p - 1)! : ZMod p) = -1 := by
     · apply Nat.pos_of_ne_zero; rw [← @val_zero p]
       intro h; apply Units.ne_zero a (val_injective p h)
     · exact val_lt _
-  · rintro a -; simp only [cast_id, nat_cast_val]
   · intro _ _ _ _ h; rw [Units.ext_iff]; exact val_injective p h
   · intro b hb
     rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, Nat.add_one_sub_one, pos_iff_ne_zero] at hb
@@ -67,6 +66,7 @@ theorem wilsons_lemma : ((p - 1)! : ZMod p) = -1 := by
     · intro h; apply hb.1; apply_fun val at h
       simpa only [val_cast_of_lt hb.right, val_zero] using h
     · simp only [val_cast_of_lt hb.right, Units.val_mk0]
+  · rintro a -; simp only [cast_id, nat_cast_val]
 #align zmod.wilsons_lemma ZMod.wilsons_lemma
 
 @[simp]
diff --git a/Mathlib/Probability/StrongLaw.lean b/Mathlib/Probability/StrongLaw.lean
index ef94f9d48f0e0..b383b9836cc94 100644
--- a/Mathlib/Probability/StrongLaw.lean
+++ b/Mathlib/Probability/StrongLaw.lean
@@ -242,16 +242,8 @@ theorem sum_prob_mem_Ioc_le {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0
         exact continuous_const.intervalIntegrable _ _
       _ = ∑ i in range N, ∑ j in range (min (i + 1) K), ∫ _ in i..(i + 1 : ℕ), (1 : ℝ) ∂ρ := by
         simp_rw [sum_sigma']
-        refine' sum_bij' (fun (p : Σ _ : ℕ, ℕ) _ => (⟨p.2, p.1⟩ : Σ _ : ℕ, ℕ)) _ (fun a _ => rfl)
-          (fun (p : Σ _ : ℕ, ℕ) _ => (⟨p.2, p.1⟩ : Σ _ : ℕ, ℕ)) _ _ _
-        · rintro ⟨i, j⟩ hij
-          simp only [mem_sigma, mem_range, mem_Ico] at hij
-          simp only [hij, Nat.lt_succ_iff.2 hij.2.1, mem_sigma, mem_range, lt_min_iff, and_self_iff]
-        · rintro ⟨i, j⟩ hij
-          simp only [mem_sigma, mem_range, lt_min_iff] at hij
-          simp only [hij, Nat.lt_succ_iff.1 hij.2.1, mem_sigma, mem_range, mem_Ico, and_self_iff]
-        · rintro ⟨i, j⟩ hij; rfl
-        · rintro ⟨i, j⟩ hij; rfl
+        refine' sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) _ _ _ _ _ <;>
+          aesop (add simp Nat.lt_succ_iff)
       _ ≤ ∑ i in range N, (i + 1) * ∫ _ in i..(i + 1 : ℕ), (1 : ℝ) ∂ρ := by
         apply sum_le_sum fun i _ => ?_
         simp only [Nat.cast_add, Nat.cast_one, sum_const, card_range, nsmul_eq_mul, Nat.cast_min]
@@ -354,16 +346,8 @@ theorem sum_variance_truncation_le {X : Ω → ℝ} (hint : Integrable X) (hnonn
       exact (continuous_id.pow _).intervalIntegrable _ _
     _ = ∑ k in range K, (∑ j in Ioo k K, ((j : ℝ) ^ 2)⁻¹) * ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by
       simp_rw [mul_sum, sum_mul, sum_sigma']
-      refine' sum_bij' (fun (p : Σ _ : ℕ, ℕ) _ => (⟨p.2, p.1⟩ : Σ _ : ℕ, ℕ)) _ (fun a _ => rfl)
-        (fun (p : Σ _ : ℕ, ℕ) _ => (⟨p.2, p.1⟩ : Σ _ : ℕ, ℕ)) _ _ _
-      · rintro ⟨i, j⟩ hij
-        simp only [mem_sigma, mem_range, mem_filter] at hij
-        simp [hij, mem_sigma, mem_range, and_self_iff, hij.2.trans hij.1]
-      · rintro ⟨i, j⟩ hij
-        simp only [mem_sigma, mem_range, mem_Ioo] at hij
-        simp only [hij, mem_sigma, mem_range, and_self_iff]
-      · rintro ⟨i, j⟩ hij; rfl
-      · rintro ⟨i, j⟩ hij; rfl
+      refine' sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) _ _ _ _ _ <;>
+        aesop (add unsafe lt_trans)
     _ ≤ ∑ k in range K, 2 / (k + 1 : ℝ) * ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by
       apply sum_le_sum fun k _ => ?_
       refine' mul_le_mul_of_nonneg_right (sum_Ioo_inv_sq_le _ _) _
@@ -458,17 +442,11 @@ theorem strong_law_aux1 {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) :
       _ = ∑ j in range (u (N - 1)),
           (∑ i in (range N).filter fun i => j < u i, ((u i : ℝ) ^ 2)⁻¹) * Var[Y j] := by
         simp_rw [mul_sum, sum_mul, sum_sigma']
-        refine' sum_bij' (fun (p : Σ _ : ℕ, ℕ) _ => (⟨p.2, p.1⟩ : Σ _ : ℕ, ℕ)) _ (fun a _ => rfl)
-          (fun (p : Σ _ : ℕ, ℕ) _ => (⟨p.2, p.1⟩ : Σ _ : ℕ, ℕ)) _ _ _
-        · rintro ⟨i, j⟩ hij
-          simp only [mem_sigma, mem_range] at hij
-          simp only [hij.1, hij.2, mem_sigma, mem_range, mem_filter, and_true_iff]
-          exact hij.2.trans_le (u_mono (Nat.le_sub_one_of_lt hij.1))
-        · rintro ⟨i, j⟩ hij
-          simp only [mem_sigma, mem_range, mem_filter] at hij
-          simp only [hij.2.1, hij.2.2, mem_sigma, mem_range, and_self_iff]
-        · rintro ⟨i, j⟩ hij; rfl
-        · rintro ⟨i, j⟩ hij; rfl
+        refine' sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) _ _ _ _ _
+        · simp only [mem_sigma, mem_range, filter_congr_decidable, mem_filter, and_imp,
+            Sigma.forall]
+          exact fun a b haN hb ↦ ⟨hb.trans_le $ u_mono $ Nat.le_pred_of_lt haN, haN, hb⟩
+        all_goals aesop
       _ ≤ ∑ j in range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j] := by
         apply sum_le_sum fun j hj => ?_
         rcases @eq_zero_or_pos _ _ j with (rfl | hj)
diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean
index 113aada14e678..ef1f4f28f3aa8 100644
--- a/Mathlib/RingTheory/Discriminant.lean
+++ b/Mathlib/RingTheory/Discriminant.lean
@@ -257,35 +257,20 @@ theorem discr_powerBasis_eq_norm [IsSeparable K L] :
         (IsAlgClosed.splits_codomain _) (hroots σ),
       ← Finset.prod_mk _ (hnodup.erase _)]
   rw [prod_sigma', prod_sigma']
-  refine'
-    prod_bij (fun i _ => ⟨e i.2, e i.1 pb.gen⟩) (fun i hi => _) (fun i _ => by simp)
-      (fun i j hi hj hij => _) fun σ hσ => _
-  · simp only [true_and_iff, Finset.mem_mk, mem_univ, mem_sigma]
-    rw [Multiset.mem_erase_of_ne fun h => ?_]
-    · exact hroots _
--- Porting note: `@mem_compl` was not necessary.
-    · simp only [true_and_iff, mem_univ, Ne.def, mem_sigma, @mem_compl _ _ _ (_),
-        mem_singleton] at hi
-      rw [← PowerBasis.liftEquiv_apply_coe, ← PowerBasis.liftEquiv_apply_coe] at h
-      exact hi (e.injective <| pb.liftEquiv.injective <| Subtype.eq h.symm)
-  · simp only [Sigma.mk.inj_iff, EmbeddingLike.apply_eq_iff_eq, heq_eq_eq] at hij
-    have h := hij.2
-    rw [← PowerBasis.liftEquiv_apply_coe, ← PowerBasis.liftEquiv_apply_coe] at h
-    refine' Sigma.eq (Equiv.injective e (Equiv.injective _ (Subtype.eq h))) (by simp [hij.1])
-  · simp only [true_and_iff, Finset.mem_mk, mem_univ, mem_sigma] at hσ ⊢
-    simp only [Sigma.exists, exists_prop, mem_compl, mem_singleton, Ne.def]
-    refine' ⟨e.symm (PowerBasis.lift pb σ.2 _), e.symm σ.1, ⟨_, Sigma.eq _ _⟩⟩
-    · rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def, ← mem_roots]
-      · exact Multiset.erase_subset _ _ hσ
-      · simp [minpoly.ne_zero (IsSeparable.isIntegral K pb.gen)]
--- Porting note: the `simp only` was not needed.
-    · simp only [@mem_compl _ _ _ (_), mem_singleton]
-      intro h
-      replace h := AlgHom.congr_fun (Equiv.injective _ h) pb.gen
-      rw [PowerBasis.lift_gen] at h
-      rw [← h] at hσ
-      exact hnodup.not_mem_erase hσ
-    all_goals simp
+  refine prod_bij' (fun i _ ↦ ⟨e i.2, e i.1 pb.gen⟩)
+    (fun σ hσ ↦ ⟨e.symm (PowerBasis.lift pb σ.2 ?_), e.symm σ.1⟩) ?_ ?_ ?_ ?_ (fun i _ ↦ by simp)
+  -- Porting note: `@mem_compl` was not necessary.
+    <;> simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def, mem_roots',
+      minpoly.ne_zero (IsSeparable.isIntegral K pb.gen), not_false_eq_true, mem_singleton, true_and,
+      @mem_compl _ _ _ (_), Sigma.forall, Equiv.apply_symm_apply, PowerBasis.lift_gen, and_imp,
+      implies_true, forall_const, Equiv.symm_apply_apply, Sigma.ext_iff, Equiv.symm_apply_eq,
+      heq_eq_eq, and_true] at *
+  · simpa only [aeval_def, eval₂_eq_eval_map] using hσ.2.2
+  · exact fun a b hba ↦ ⟨fun h ↦ hba $ e.injective $ pb.algHom_ext h.symm, hroots _⟩
+  · rintro a b hba ha
+    rw [ha, PowerBasis.lift_gen] at hba
+    exact hba.1 rfl
+  · exact fun a b _ ↦ pb.algHom_ext $ pb.lift_gen _ _
 #align algebra.discr_power_basis_eq_norm Algebra.discr_powerBasis_eq_norm
 
 section Integral
diff --git a/Mathlib/RingTheory/HahnSeries.lean b/Mathlib/RingTheory/HahnSeries.lean
index 4b7f1888ec2d3..065e09cd5e742 100644
--- a/Mathlib/RingTheory/HahnSeries.lean
+++ b/Mathlib/RingTheory/HahnSeries.lean
@@ -780,27 +780,9 @@ private theorem mul_assoc' [NonUnitalSemiring R] (x y z : HahnSeries Γ R) :
   rw [mul_coeff_left' (x.isPwo_support.add y.isPwo_support) support_mul_subset_add_support,
     mul_coeff_right' (y.isPwo_support.add z.isPwo_support) support_mul_subset_add_support]
   simp only [mul_coeff, add_coeff, sum_mul, mul_sum, sum_sigma']
-  refine' sum_bij_ne_zero (fun a _ _ => ⟨⟨a.2.1, a.2.2 + a.1.2⟩, ⟨a.2.2, a.1.2⟩⟩) _ _ _ _
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ H1 H2
-    simp only [and_true_iff, Set.image2_add, eq_self_iff_true, mem_addAntidiagonal, Ne.def,
-      Set.image_prod, mem_sigma, Set.mem_setOf_eq] at H1 H2 ⊢
-    obtain ⟨⟨H3, nz, rfl⟩, nx, ny, rfl⟩ := H1
-    exact ⟨⟨nx, Set.add_mem_add ny nz, (add_assoc _ _ _).symm⟩, ny, nz⟩
-  · rintro ⟨⟨i1, j1⟩, k1, l1⟩ ⟨⟨i2, j2⟩, k2, l2⟩ H1 H2 H3 H4 H5
-    simp only [Set.image2_add, Prod.mk.inj_iff, mem_addAntidiagonal, Ne.def, Set.image_prod,
-      mem_sigma, Set.mem_setOf_eq, heq_iff_eq] at H1 H3 H5
-    obtain (⟨⟨rfl, _⟩, rfl, rfl⟩ : (k1 = k2 ∧ l1 + j1 = l2 + j2) ∧ l1 = l2 ∧ j1 = j2) :=
-      by simpa using H5
-    simp only [and_true_iff, Prod.mk.inj_iff, eq_self_iff_true, heq_iff_eq, ← H1.2.2.2, ← H3.2.2.2]
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ H1 H2
-    simp only [exists_prop, Set.image2_add, Prod.mk.inj_iff, mem_addAntidiagonal, Sigma.exists,
-      Ne.def, Set.image_prod, mem_sigma, Set.mem_setOf_eq, heq_iff_eq, Prod.exists] at H1 H2 ⊢
-    obtain ⟨⟨nx, H, rfl⟩, ny, nz, rfl⟩ := H1
-    exact
-      ⟨i + k, l, i, k, ⟨⟨Set.add_mem_add nx ny, nz, add_assoc _ _ _⟩ , nx, ny, rfl⟩,
-        fun h => H2 <| by rw [← h, mul_assoc], rfl⟩
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ _ _
-    simp [mul_assoc]
+  apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
+    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;>
+    aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])
 
 instance [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (HahnSeries Γ R) :=
   { inferInstanceAs (AddCommMonoid (HahnSeries Γ R)),
@@ -830,15 +812,12 @@ instance [Semiring R] : Semiring (HahnSeries Γ R) :=
   { inferInstanceAs (NonAssocSemiring (HahnSeries Γ R)),
     inferInstanceAs (NonUnitalSemiring (HahnSeries Γ R)) with }
 
-instance [NonUnitalCommSemiring R] : NonUnitalCommSemiring (HahnSeries Γ R) :=
-  { inferInstanceAs (NonUnitalSemiring (HahnSeries Γ R)) with
-    mul_comm := fun x y => by
-      ext
-      simp_rw [mul_coeff, mul_comm]
-      refine'
-          sum_bij (fun a _ => a.swap) (fun a ha => _) (fun a _ => rfl)
-            (fun _ _ _ _ => Prod.swap_inj.1) fun a ha => ⟨a.swap, _, a.swap_swap.symm⟩ <;>
-        rwa [swap_mem_addAntidiagonal] }
+instance [NonUnitalCommSemiring R] : NonUnitalCommSemiring (HahnSeries Γ R) where
+  __ : NonUnitalSemiring (HahnSeries Γ R) := inferInstance
+  mul_comm x y := by
+    ext
+    simp_rw [mul_coeff, mul_comm]
+    exact Finset.sum_equiv (Equiv.prodComm _ _) (fun _ ↦ swap_mem_addAntidiagonal.symm) $ by simp
 
 instance [CommSemiring R] : CommSemiring (HahnSeries Γ R) :=
   { inferInstanceAs (NonUnitalCommSemiring (HahnSeries Γ R)),
diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean
index 813c6e500a38b..5eb43c6b4eca0 100644
--- a/Mathlib/RingTheory/IntegralDomain.lean
+++ b/Mathlib/RingTheory/IntegralDomain.lean
@@ -255,15 +255,14 @@ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0
       (∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R))
         = ∑ n in range (orderOf x), ((x : Rˣ) : R) ^ n :=
         Eq.symm <|
-          sum_bij (fun n _ => x ^ n) (by simp only [mem_univ, forall_true_iff])
-            (by simp only [imp_true_iff, eq_self_iff_true, Subgroup.coe_pow,
-                Units.val_pow_eq_pow_val])
-            (fun m n hm hn => pow_injOn_Iio_orderOf (by simpa only [mem_range] using hm)
-                (by simpa only [mem_range] using hn))
+          sum_nbij (x ^ ·) (by simp only [mem_univ, forall_true_iff])
+            (by simpa using pow_injOn_Iio_orderOf)
             (fun b _ => let ⟨n, hn⟩ := hx b
               ⟨n % orderOf x, mem_range.2 (Nat.mod_lt _ (orderOf_pos _)),
                -- Porting note: have to use `dsimp` to apply the function
                by dsimp at hn ⊢; rw [pow_mod_orderOf, hn]⟩)
+            (by simp only [imp_true_iff, eq_self_iff_true, Subgroup.coe_pow,
+                Units.val_pow_eq_pow_val])
       _ = 0 := ?_
 
     rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]
diff --git a/Mathlib/RingTheory/Noetherian.lean b/Mathlib/RingTheory/Noetherian.lean
index 33ec72b17b6dc..3eef173dc2b31 100644
--- a/Mathlib/RingTheory/Noetherian.lean
+++ b/Mathlib/RingTheory/Noetherian.lean
@@ -588,7 +588,7 @@ theorem isNoetherian_of_fg_of_noetherian {R M} [Ring R] [AddCommGroup M] [Module
     rcases hn with ⟨l, hl1, hl2⟩
     refine' ⟨fun x => l x, Subtype.ext _⟩
     change (∑ i in s.attach, l i • (i : M)) = n
-    rw [@Finset.sum_attach M M s _ fun i => l i • i, ← hl2,
+    rw [s.sum_attach fun i ↦ l i • i, ← hl2,
       Finsupp.total_apply, Finsupp.sum, eq_comm]
     refine' Finset.sum_subset hl1 fun x _ hx => _
     rw [Finsupp.not_mem_support_iff.1 hx, zero_smul]
diff --git a/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean b/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
index 72a6ae6b66fab..90be3c5eb3061 100644
--- a/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
+++ b/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
@@ -119,7 +119,7 @@ theorem integralNormalization_eval₂_eq_zero {p : R[X]} (f : R →+* S) {z : S}
           f (coeff (integralNormalization p) i.1 * p.leadingCoeff ^ i.1) * z ^ i.1 := by
       rw [eval₂_eq_sum, sum_def, support_integralNormalization]
       simp only [mul_comm z, mul_pow, mul_assoc, RingHom.map_pow, RingHom.map_mul]
-      exact Finset.sum_attach.symm
+      rw [← Finset.sum_attach]
     _ =
         p.support.attach.sum fun i =>
           f (coeff p i.1 * p.leadingCoeff ^ (natDegree p - 1)) * z ^ i.1 := by
@@ -141,7 +141,7 @@ theorem integralNormalization_eval₂_eq_zero {p : R[X]} (f : R →+* S) {z : S}
       simp_rw [eval₂_eq_sum, sum_def, fun i => mul_comm (coeff p i), RingHom.map_mul,
                RingHom.map_pow, mul_assoc, ← Finset.mul_sum]
       congr 1
-      exact @Finset.sum_attach _ _ p.support _ fun i => f (p.coeff i) * z ^ i
+      exact p.support.sum_attach fun i ↦ f (p.coeff i) * z ^ i
     _ = 0 := by rw [hz, mul_zero]
 #align polynomial.integral_normalization_eval₂_eq_zero Polynomial.integralNormalization_eval₂_eq_zero
 
diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
index 4004fcbd02b49..42b7957cbec84 100644
--- a/Mathlib/RingTheory/PowerSeries/Basic.lean
+++ b/Mathlib/RingTheory/PowerSeries/Basic.lean
@@ -298,27 +298,8 @@ protected theorem mul_assoc (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * 
   ext1 n
   classical
   simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']
-  refine' Finset.sum_bij (fun p _ => ⟨(p.2.1, p.2.2 + p.1.2), (p.2.2, p.1.2)⟩) _ _ _ _ <;>
-    simp only [mem_antidiagonal, Finset.mem_sigma, heq_iff_eq, Prod.mk.inj_iff, and_imp,
-      exists_prop]
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩
-    dsimp only
-    rintro rfl rfl
-    simp [add_assoc]
-  · rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩
-    dsimp only
-    rintro rfl rfl
-    apply mul_assoc
-  · rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩ ⟨⟨i, j⟩, ⟨k, l⟩⟩
-    dsimp only
-    rintro rfl rfl - rfl
-    simp only [Sigma.mk.inj_iff, Prod.mk.injEq, heq_iff_eq, and_imp]
-    rintro rfl - rfl rfl
-    simp only [and_self]
-  · rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩
-    dsimp only
-    rintro rfl rfl
-    refine' ⟨⟨(i + k, l), (i, k)⟩, _, _⟩ <;> simp [add_assoc]
+  apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
+    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;> aesop (add simp [add_assoc, mul_assoc])
 #align mv_power_series.mul_assoc MvPowerSeries.mul_assoc
 
 instance : Semiring (MvPowerSeries σ R) :=
@@ -1975,35 +1956,21 @@ theorem coeff_inv_aux (n : ℕ) (a : R) (φ : R⟦X⟧) :
   split_ifs; · rfl
   congr 1
   symm
-  apply Finset.sum_bij fun (p : ℕ × ℕ) _h => (single () p.1, single () p.2)
-  · rintro ⟨i, j⟩ hij
-    rw [mem_antidiagonal] at hij
-    rw [mem_antidiagonal, ← Finsupp.single_add, hij]
+  apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b))
+    fun (f, g) ↦ (f (), g ())
+  · aesop
+  · aesop
+  · aesop
+  · aesop
   · rintro ⟨i, j⟩ _hij
-    by_cases H : j < n
-    · rw [if_pos H, if_pos]
-      · rfl
-      constructor
-      · rintro ⟨⟩
-        simpa [Finsupp.single_eq_same] using le_of_lt H
-      · intro hh
-        rw [lt_iff_not_ge] at H
-        apply H
-        simpa [Finsupp.single_eq_same] using hh ()
-    · rw [if_neg H, if_neg]
-      rintro ⟨_h₁, h₂⟩
-      apply h₂
-      rintro ⟨⟩
-      simpa [Finsupp.single_eq_same] using not_lt.1 H
-  · rintro ⟨i, j⟩ ⟨k, l⟩ _hij _hkl
-    simpa only [Prod.mk.inj_iff, Finsupp.unique_single_eq_iff] using id
-  · rintro ⟨f, g⟩ hfg
-    refine' ⟨(f (), g ()), _, _⟩
-    · rw [mem_antidiagonal] at hfg
-      rw [mem_antidiagonal, ← Finsupp.add_apply, hfg, Finsupp.single_eq_same]
-    · rw [Prod.mk.inj_iff]
-      dsimp
-      exact ⟨Finsupp.unique_single f, Finsupp.unique_single g⟩
+    obtain H | H := le_or_lt n j
+    · aesop
+    rw [if_pos H, if_pos]
+    · rfl
+    refine ⟨?_, fun hh ↦ H.not_le ?_⟩
+    · rintro ⟨⟩
+      simpa [Finsupp.single_eq_same] using le_of_lt H
+    · simpa [Finsupp.single_eq_same] using hh ()
 #align power_series.coeff_inv_aux PowerSeries.coeff_inv_aux
 
 /-- A formal power series is invertible if the constant coefficient is invertible.-/