feat(Algebra): add abstract prod_apply and FunLike.coe_prod

Mathlib/Algebra/BigOperators/Pi.lean

@@ -12,6 +12,7 @@ public import Mathlib.Algebra.Group.Action.Pi
 public import Mathlib.Algebra.Notation.Indicator
 public import Mathlib.Algebra.Ring.Pi
 public import Mathlib.Data.Fintype.Basic
+public import Mathlib.Data.FunLike.IsApply
 
 /-!
 # Big operators for Pi Types
@@ -230,3 +231,21 @@ theorem eqOn_fun_finsetProd {ι α β : Type*} [CommMonoid α]
   convert eqOn_finsetProd h v <;> simp
 
 end EqOn
+
+section FunLike
+
+variable {F α β ι : Type*} [FunLike F α β] [CommMonoid β] [CommMonoid F]
+  [IsOneApply F α β] [IsMulApply F α β]
+
+open Classical in
+@[to_additive (attr := simp, grind =)]
+theorem prod_apply (s : Finset ι) (f : ι → F) (x : α) : (∏ i ∈ s, f i) x = ∏ i ∈ s, f i x := by
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert i s his h => simp [his, h]
+
+@[to_additive (attr := norm_cast)]
+theorem FunLike.coe_prod (s : Finset ι) (f : ι → F) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, (f i : α → β) := by
+  ext; simp
+
+end FunLike

Mathlib/Analysis/Calculus/FDeriv/Add.lean

@@ -192,7 +192,7 @@ section Add
 theorem HasFDerivAtFilter.add (hf : HasFDerivAtFilter f f' L)
     (hg : HasFDerivAtFilter g g' L) : HasFDerivAtFilter (f + g) (f' + g') L :=
   .of_isLittleO <| (hf.isLittleO.add hg.isLittleO).congr_left fun _ => by
-    grind [Pi.add_apply, add_apply]
+    grind [Pi.add_apply, ContinuousLinearMap.add_apply]
 
 @[to_fun (attr := fun_prop)]
 theorem HasStrictFDerivAt.add (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :

Mathlib/Data/Matrix/PEquiv.lean

@@ -161,7 +161,7 @@ theorem toMatrix_swap [DecidableEq n] [AddGroupWithOne α] (i j : n) :
       (1 : Matrix n n α) - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix +
         (single j i).toMatrix := by
   ext
-  dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, one_apply]
+  dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, Matrix.one_apply]
   split_ifs <;> simp_all
 
 @[simp]

Mathlib/LinearAlgebra/Matrix/Polynomial.lean

@@ -56,7 +56,7 @@ theorem natDegree_det_X_add_C_le (A B : Matrix n n α) :
         (X • A.map C + B.map C : Matrix n n α[X]) (g i) i)
     _ ≤ Finset.univ.card • 1 := (Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_)
     _ ≤ Fintype.card n := by simp [mul_one, Finset.card_univ]
-  dsimp only [add_apply, smul_apply, map_apply, smul_eq_mul]
+  dsimp only [Matrix.add_apply, Matrix.smul_apply, map_apply, smul_eq_mul]
   compute_degree
 
 theorem coeff_det_X_add_C_zero (A B : Matrix n n α) :
@@ -80,7 +80,7 @@ theorem coeff_det_X_add_C_card (A B : Matrix n n α) :
   convert (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm
   · simp [coeff_C]
   · rintro p -
-    dsimp only [add_apply, smul_apply, map_apply, smul_eq_mul]
+    dsimp only [Matrix.add_apply, Matrix.smul_apply, map_apply, smul_eq_mul]
     compute_degree
 
 theorem leadingCoeff_det_X_one_add_C (A : Matrix n n α) :

Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

@@ -142,7 +142,8 @@ def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] :
     dsimp only [LinearMap.smul_apply, LinearMap.coe_mk, AddHom.coe_mk, AddHom.toFun_eq_coe,
       LinearMap.coe_toAddHom, LinearMap.prod_apply, Function.prod_apply, LinearMap.add_apply,
       LinearMap.coe_comp, Function.comp_apply, LinearMap.fst_apply, LinearMap.snd_apply,
-      LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, prod_apply, neg_apply]
+      LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, QuadraticMap.prod_apply,
+      QuadraticMap.neg_apply]
     simp only [polar_sub_right, polar_self, nsmul_eq_mul, Nat.cast_ofNat, polar_comm _ x.1 x.2,
       smul_sub, Module.End.smul_def, sub_add_sub_cancel, ← sub_eq_add_neg (Q x.1) (Q x.2)]
     rw [← map_sub (⅟2 : Module.End R R), ← mul_sub, ← Module.End.smul_def]