chore: Make Finset.prod_product and Fintype.prod_prod_type more uniform (#16884)

Make more variables explicit in the rewriting lemmas. Unsimp `Fintype.prod_prod_type` since `Finset.prod_product` is not simp.

Author: YaelDillies

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -776,26 +776,26 @@ lemma prod_mul_prod_comm (f g h i : α → β) :
   simp_rw [prod_mul_distrib, mul_mul_mul_comm]
 
 @[to_additive]
-theorem prod_product {s : Finset γ} {t : Finset α} {f : γ × α → β} :
+theorem prod_product (s : Finset γ) (t : Finset α) (f : γ × α → β) :
     ∏ x ∈ s ×ˢ t, f x = ∏ x ∈ s, ∏ y ∈ t, f (x, y) :=
   prod_finset_product (s ×ˢ t) s (fun _a => t) fun _p => mem_product
 
 /-- An uncurried version of `Finset.prod_product`. -/
 @[to_additive "An uncurried version of `Finset.sum_product`"]
-theorem prod_product' {s : Finset γ} {t : Finset α} {f : γ → α → β} :
+theorem prod_product' (s : Finset γ) (t : Finset α) (f : γ → α → β) :
     ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ x ∈ s, ∏ y ∈ t, f x y :=
-  prod_product
+  prod_product ..
 
 @[to_additive]
-theorem prod_product_right {s : Finset γ} {t : Finset α} {f : γ × α → β} :
+theorem prod_product_right (s : Finset γ) (t : Finset α) (f : γ × α → β) :
     ∏ x ∈ s ×ˢ t, f x = ∏ y ∈ t, ∏ x ∈ s, f (x, y) :=
   prod_finset_product_right (s ×ˢ t) t (fun _a => s) fun _p => mem_product.trans and_comm
 
 /-- An uncurried version of `Finset.prod_product_right`. -/
 @[to_additive "An uncurried version of `Finset.sum_product_right`"]
-theorem prod_product_right' {s : Finset γ} {t : Finset α} {f : γ → α → β} :
+theorem prod_product_right' (s : Finset γ) (t : Finset α) (f : γ → α → β) :
     ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ y ∈ t, ∏ x ∈ s, f x y :=
-  prod_product_right
+  prod_product_right ..
 
 /-- Generalization of `Finset.prod_comm` to the case when the inner `Finset`s depend on the outer
 variable. -/

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -396,7 +396,7 @@ theorem mul_apply_antidiagonal [Mul G] (f g : MonoidAlgebra k G) (x : G) (s : Fi
       let F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
       calc
         (f * g) x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := mul_apply f g x
-        _ = ∑ p ∈ f.support ×ˢ g.support, F p := Finset.sum_product.symm
+        _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
         _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G => p.1 * p.2 = x, f p.1 * g p.2 :=
           (Finset.sum_filter _ _).symm
         _ = ∑ p ∈ s.filter fun p : G × G => p.1 ∈ f.support ∧ p.2 ∈ g.support, f p.1 * g p.2 :=

Mathlib/Data/Fintype/BigOperators.lean

@@ -224,26 +224,26 @@ theorem Fintype.prod_sum_type (f : α₁ ⊕ α₂ → M) :
     ∏ x, f x = (∏ a₁, f (Sum.inl a₁)) * ∏ a₂, f (Sum.inr a₂) :=
   prod_disj_sum _ _ _
 
-@[to_additive (attr := simp) Fintype.sum_prod_type]
-theorem Fintype.prod_prod_type [CommMonoid γ] {f : α₁ × α₂ → γ} :
+@[to_additive Fintype.sum_prod_type]
+theorem Fintype.prod_prod_type [CommMonoid γ] (f : α₁ × α₂ → γ) :
     ∏ x, f x = ∏ x, ∏ y, f (x, y) :=
-  Finset.prod_product
+  Finset.prod_product ..
 
 /-- An uncurried version of `Finset.prod_prod_type`. -/
 @[to_additive Fintype.sum_prod_type' "An uncurried version of `Finset.sum_prod_type`"]
-theorem Fintype.prod_prod_type' [CommMonoid γ] {f : α₁ → α₂ → γ} :
+theorem Fintype.prod_prod_type' [CommMonoid γ] (f : α₁ → α₂ → γ) :
     ∏ x : α₁ × α₂, f x.1 x.2 = ∏ x, ∏ y, f x y :=
-  Finset.prod_product'
+  Finset.prod_product' ..
 
 @[to_additive Fintype.sum_prod_type_right]
-theorem Fintype.prod_prod_type_right [CommMonoid γ] {f : α₁ × α₂ → γ} :
+theorem Fintype.prod_prod_type_right [CommMonoid γ] (f : α₁ × α₂ → γ) :
     ∏ x, f x = ∏ y, ∏ x, f (x, y) :=
-  Finset.prod_product_right
+  Finset.prod_product_right ..
 
 /-- An uncurried version of `Finset.prod_prod_type_right`. -/
 @[to_additive Fintype.sum_prod_type_right' "An uncurried version of `Finset.sum_prod_type_right`"]
-theorem Fintype.prod_prod_type_right' [CommMonoid γ] {f : α₁ → α₂ → γ} :
+theorem Fintype.prod_prod_type_right' [CommMonoid γ] (f : α₁ → α₂ → γ) :
     ∏ x : α₁ × α₂, f x.1 x.2 = ∏ y, ∏ x, f x y :=
-  Finset.prod_product_right'
+  Finset.prod_product_right' ..
 
 end

Mathlib/Data/Matrix/Composition.lean

@@ -55,9 +55,7 @@ variable [Semiring R] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
 @[simps!]
 def compRingEquiv : Matrix I I (Matrix J J R) ≃+* Matrix (I × J) (I × J) R where
   __ := Matrix.compAddEquiv I I J J R
-  map_mul' _ _ := by
-    ext _ _
-    exact (Matrix.sum_apply _ _ _ _).trans <| Eq.symm Fintype.sum_prod_type
+  map_mul' _ _ := by ext; exact (Matrix.sum_apply ..).trans <| .symm <| Fintype.sum_prod_type ..
 
 end Semiring
 

Mathlib/LinearAlgebra/Matrix/Trace.lean

@@ -109,7 +109,7 @@ theorem _root_.AddMonoidHom.map_trace [AddCommMonoid S] (f : R →+ S) (A : Matr
 
 lemma trace_blockDiagonal [DecidableEq p] (M : p → Matrix n n R) :
     trace (blockDiagonal M) = ∑ i, trace (M i) := by
-  simp [blockDiagonal, trace, Finset.sum_comm (γ := n)]
+  simp [blockDiagonal, trace, Finset.sum_comm (γ := n), Fintype.sum_prod_type]
 
 lemma trace_blockDiagonal' [DecidableEq p] {m : p → Type*} [∀ i, Fintype (m i)]
     (M : ∀ i, Matrix (m i) (m i) R) :

Mathlib/RingTheory/MatrixAlgebra.lean

@@ -96,13 +96,13 @@ theorem invFun_algebraMap (M : Matrix n n R) : invFun R A n (M.map (algebraMap R
   simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum, mul_boole]
   congr
   conv_rhs => rw [matrix_eq_sum_stdBasisMatrix M]
-  convert Finset.sum_product (β := Matrix n n R); simp
+  convert Finset.sum_product (β := Matrix n n R) ..; simp
 
 theorem right_inv (M : Matrix n n A) : (toFunAlgHom R A n) (invFun R A n M) = M := by
   simp only [invFun, map_sum, stdBasisMatrix, apply_ite ↑(algebraMap R A), smul_eq_mul,
     mul_boole, toFunAlgHom_apply, RingHom.map_zero, RingHom.map_one, Matrix.map_apply,
     Pi.smul_def]
-  convert Finset.sum_product (β := Matrix n n A)
+  convert Finset.sum_product (β := Matrix n n A) ..
   conv_lhs => rw [matrix_eq_sum_stdBasisMatrix M]
   refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => Matrix.ext fun a b => ?_
   simp only [stdBasisMatrix, smul_apply, Matrix.map_apply]