chore: clean up uses of Pi.smul_apply (#9970)

After #9949, `Pi.smul_apply` can be used in `simp` again. This PR cleans up some workarounds.
leanprover-community · Feb 12, 2024 · 105a8c5 · 105a8c5
1 parent fa3313a
commit 105a8c5
Show file tree

Hide file tree

Showing 9 changed files with 11 additions and 12 deletions.
diff --git a/Mathlib/GroupTheory/GroupAction/Pi.lean b/Mathlib/GroupTheory/GroupAction/Pi.lean
@@ -270,10 +270,9 @@ theorem Function.extend_smul {R α β γ : Type*} [SMul R γ] (r : R) (f : α
   funext fun x => by
   -- Porting note: Lean4 is unable to automatically call `Classical.propDecidable`
   haveI : Decidable (∃ a : α, f a = x) := Classical.propDecidable _
-  rw [extend_def, Pi.smul_apply, Pi.smul_apply, extend_def]
+  simp only [extend_def, Pi.smul_apply]
   split_ifs <;>
   rfl
-  -- convert (apply_dite (fun c : γ => r • c) _ _ _).symm
 #align function.extend_smul Function.extend_smul
 #align function.extend_vadd Function.extend_vadd
 

diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean
@@ -321,7 +321,7 @@ noncomputable def basisSingleton (ι : Type*) [Unique ι] (h : finrank K V = 1)
         apply_fun b.repr using b.repr.toEquiv.injective
         apply_fun Equiv.finsuppUnique
         simp only [LinearEquiv.map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
-          RingHom.id_apply, smul_eq_mul, Pi.smul_apply, Equiv.finsuppUnique_apply]
+          smul_eq_mul, Pi.smul_apply, Equiv.finsuppUnique_apply]
         exact div_mul_cancel _ h
       right_inv := fun f => by
         ext

diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -613,7 +613,8 @@ theorem LinearIndependent.group_smul {G : Type*} [hG : Group G] [DistribMulActio
     exact (hgs i hi).symm ▸ smul_zero _
   · rw [← hsum, Finset.sum_congr rfl _]
     intros
-    erw [Pi.smul_apply, smul_assoc, smul_comm]
+    dsimp
+    rw [smul_assoc, smul_comm]
 #align linear_independent.group_smul LinearIndependent.group_smul
 
 -- This lemma cannot be proved with `LinearIndependent.group_smul` since the action of

diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
@@ -438,7 +438,7 @@ theorem lpMeasToLpTrim_smul (hm : m ≤ m0) (c : 𝕜) (f : lpMeas F 𝕜 m p μ
   refine' (lpMeasToLpTrim_ae_eq hm _).trans _
   refine' (Lp.coeFn_smul _ _).trans _
   refine' (lpMeasToLpTrim_ae_eq hm f).mono fun x hx => _
-  rw [Pi.smul_apply, Pi.smul_apply, hx]
+  simp only [Pi.smul_apply, hx]
 #align measure_theory.Lp_meas_to_Lp_trim_smul MeasureTheory.lpMeasToLpTrim_smul
 
 /-- `lpMeasSubgroupToLpTrim` preserves the norm. -/

diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
@@ -310,7 +310,7 @@ theorem condexp_smul (c : 𝕜) (f : α → F') : μ[c • f|m] =ᵐ[μ] c •
   rw [condexpL1_smul c f]
   refine' (@condexp_ae_eq_condexpL1 _ _ _ _ _ m _ _ hm _ f).mp _
   refine' (coeFn_smul c (condexpL1 hm μ f)).mono fun x hx1 hx2 => _
-  rw [hx1, Pi.smul_apply, Pi.smul_apply, hx2]
+  simp only [hx1, hx2, Pi.smul_apply]
 #align measure_theory.condexp_smul MeasureTheory.condexp_smul
 
 theorem condexp_neg (f : α → F') : μ[-f|m] =ᵐ[μ] -μ[f|m] := by

diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
@@ -110,7 +110,7 @@ theorem condexpIndL1Fin_smul (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c :
   rw [condexpIndSMul_smul hs hμs c x]
   refine' (Lp.coeFn_smul _ _).trans _
   refine' (condexpIndL1Fin_ae_eq_condexpIndSMul hm hs hμs x).mono fun y hy => _
-  rw [Pi.smul_apply, Pi.smul_apply, hy]
+  simp only [Pi.smul_apply, hy]
 #align measure_theory.condexp_ind_L1_fin_smul MeasureTheory.condexpIndL1Fin_smul
 
 theorem condexpIndL1Fin_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s)
@@ -122,7 +122,7 @@ theorem condexpIndL1Fin_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs
   rw [condexpIndSMul_smul' hs hμs c x]
   refine' (Lp.coeFn_smul _ _).trans _
   refine' (condexpIndL1Fin_ae_eq_condexpIndSMul hm hs hμs x).mono fun y hy => _
-  rw [Pi.smul_apply, Pi.smul_apply, hy]
+  simp only [Pi.smul_apply, hy]
 #align measure_theory.condexp_ind_L1_fin_smul' MeasureTheory.condexpIndL1Fin_smul'
 
 theorem norm_condexpIndL1Fin_le (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :

diff --git a/Mathlib/MeasureTheory/Integral/SetIntegral.lean b/Mathlib/MeasureTheory/Integral/SetIntegral.lean
@@ -924,7 +924,7 @@ theorem Lp_toLp_restrict_smul (c : 𝕜) (f : Lp F p μ) (s : Set α) :
   refine' (Memℒp.coeFn_toLp ((Lp.memℒp (c • f)).restrict s)).mp _
   refine'
     (Lp.coeFn_smul c (Memℒp.toLp f ((Lp.memℒp f).restrict s))).mono fun x hx1 hx2 hx3 hx4 => _
-  rw [hx2, hx1, Pi.smul_apply, hx3, hx4, Pi.smul_apply]
+  simp only [hx2, hx1, hx3, hx4, Pi.smul_apply]
 set_option linter.uppercaseLean3 false in
 #align measure_theory.Lp_to_Lp_restrict_smul MeasureTheory.Lp_toLp_restrict_smul
 

diff --git a/Mathlib/Probability/Martingale/Basic.lean b/Mathlib/Probability/Martingale/Basic.lean
@@ -129,7 +129,7 @@ theorem sub (hf : Martingale f ℱ μ) (hg : Martingale g ℱ μ) : Martingale (
 theorem smul (c : ℝ) (hf : Martingale f ℱ μ) : Martingale (c • f) ℱ μ := by
   refine' ⟨hf.adapted.smul c, fun i j hij => _⟩
   refine' (condexp_smul c (f j)).trans ((hf.2 i j hij).mono fun x hx => _)
-  rw [Pi.smul_apply, hx, Pi.smul_apply, Pi.smul_apply]
+  simp only [Pi.smul_apply, hx]
 #align measure_theory.martingale.smul MeasureTheory.Martingale.smul
 
 theorem supermartingale [Preorder E] (hf : Martingale f ℱ μ) : Supermartingale f ℱ μ :=

diff --git a/Mathlib/Topology/ContinuousFunction/Algebra.lean b/Mathlib/Topology/ContinuousFunction/Algebra.lean
@@ -619,8 +619,7 @@ theorem coe_smul [SMul R M] [ContinuousConstSMul R M] (c : R) (f : C(α, M)) :
 #align continuous_map.coe_smul ContinuousMap.coe_smul
 #align continuous_map.coe_vadd ContinuousMap.coe_vadd
 
--- Porting note: adding `@[simp]` here, as `Pi.smul_apply` no longer fires.
-@[to_additive (attr := simp)]
+@[to_additive]
 theorem smul_apply [SMul R M] [ContinuousConstSMul R M] (c : R) (f : C(α, M)) (a : α) :
     (c • f) a = c • f a :=
   rfl