diff --git a/Statlib/Divergence/FDiv/Basic.lean b/Statlib/Divergence/FDiv/Basic.lean
index e524e28..8e273f3 100644
--- a/Statlib/Divergence/FDiv/Basic.lean
+++ b/Statlib/Divergence/FDiv/Basic.lean
@@ -213,7 +213,7 @@ lemma fDiv_eq_lintegral_mixtureFun (μ ν : Measure α) [SigmaFinite μ] [SigmaF
     filter_upwards [Measure.rnDeriv_eq_div_rnDeriv_add μ ν] with x hx
     rw [hx]
   have h2 : f.derivAtTop * μ N = ∫⁻ x, N.indicator (fun _ ↦ f.derivAtTop) x ∂(μ + ν) := by
-    rw [lintegral_indicator hN, setLIntegral_const, Measure.add_apply, hνN, add_zero]
+    rw [lintegral_indicator hN, setLIntegral_const, add_apply, hνN, add_zero]
   rw [fDiv, Measure.singularPart_eq_restrict_rnDeriv_add_eq_zero, Measure.restrict_apply_univ,
     h1, h2, ← lintegral_add_right _ (measurable_const.indicator hN)]
   refine lintegral_congr_ae ?_
@@ -272,7 +272,7 @@ lemma fDiv_add_measure_le (μ₁ μ₂ ν : Measure α) [SigmaFinite μ₁] [Sig
   rw [this, fDiv_absolutelyContinuous_add_mutuallySingular
       ((withDensity_absolutelyContinuous _ _).add_left (withDensity_absolutelyContinuous _ _))
       ((μ₁.mutuallySingular_singularPart _).add_left (μ₂.mutuallySingular_singularPart _))]
-  simp only [Measure.coe_add, Pi.add_apply]
+  simp only [FunLike.coe_add, Pi.add_apply]
   conv_rhs => rw [add_comm (μ₁.singularPart ν)]
   rw [fDiv_absolutelyContinuous_add_mutuallySingular (withDensity_absolutelyContinuous _ _)
     (μ₁.mutuallySingular_singularPart _)]
diff --git a/Statlib/Divergence/FDiv/CompProd.lean b/Statlib/Divergence/FDiv/CompProd.lean
index 8541ffa..7ac7104 100644
--- a/Statlib/Divergence/FDiv/CompProd.lean
+++ b/Statlib/Divergence/FDiv/CompProd.lean
@@ -77,7 +77,7 @@ lemma fDiv_prod_right (ξ : Measure β) [IsFiniteMeasure ξ] (μ ν : Measure α
     rw [← ENNReal.coe_ne_zero, hc]
     exact NeZero.ne _
   have : IsProbabilityMeasure (c⁻¹ • ξ) := ⟨by
-    rw [Measure.smul_apply, ← hc, ENNReal.smul_def, smul_eq_mul, ENNReal.coe_inv hc0,
+    rw [smul_apply, ← hc, ENNReal.smul_def, smul_eq_mul, ENNReal.coe_inv hc0,
       ENNReal.inv_mul_cancel (by simpa using hc0) ENNReal.coe_ne_top]⟩
   have h_prod (ρ : Measure α) [SFinite ρ] : ξ.prod ρ = c • (c⁻¹ • ξ).prod ρ := by
     rw [Measure.prod_smul_left, smul_smul, mul_inv_cancel₀ hc0, one_smul]
diff --git a/Statlib/Divergence/FDiv/IntegralRepresentation.lean b/Statlib/Divergence/FDiv/IntegralRepresentation.lean
index da5e59b..d41b0a2 100644
--- a/Statlib/Divergence/FDiv/IntegralRepresentation.lean
+++ b/Statlib/Divergence/FDiv/IntegralRepresentation.lean
@@ -230,7 +230,7 @@ theorem fDiv_add_eq_lintegral_fDiv_statInfoDivFun_add [IsFiniteMeasure μ] [IsFi
   have h_ac : ν.withDensity (∂μ/∂ν) ≪ ν := withDensity_absolutelyContinuous _ _
   have hμ : μ univ = ν.withDensity (∂μ/∂ν) univ + μ.singularPart ν univ := by
     conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
-    rw [Measure.add_apply, add_comm]
+    rw [add_apply, add_comm]
   have h_in : ∀ x, fDiv (statInfoDivFun 1 x) μ ν
       = fDiv (statInfoDivFun 1 x) (ν.withDensity (∂μ/∂ν)) ν
         + (statInfoDivFun 1 x).derivAtTop * μ.singularPart ν univ :=
diff --git a/Statlib/Divergence/Hellinger/Basic.lean b/Statlib/Divergence/Hellinger/Basic.lean
index 32973fa..02fe12b 100644
--- a/Statlib/Divergence/Hellinger/Basic.lean
+++ b/Statlib/Divergence/Hellinger/Basic.lean
@@ -140,7 +140,7 @@ lemma toReal_hellingerDiv_eq_integral_of_lt_one [IsFiniteMeasure μ] [IsFiniteMe
   congr 2
   rw [mul_comm a, ← mul_add]
   congr 1
-  conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, Measure.coe_add, Pi.add_apply,
+  conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, FunLike.coe_add, Pi.add_apply,
     ENNReal.toReal_add (measure_ne_top _ _) (measure_ne_top _ _)]
   simp only [MeasurableSet.univ, withDensity_apply, Measure.restrict_univ, add_left_inj]
   rw [integral_toReal]
@@ -472,7 +472,7 @@ lemma toReal_hellingerDiv_smul_left [IsFiniteMeasure μ] [IsFiniteMeasure ν]
   rw [toReal_hellingerDiv_eq_integral_of_ne_top ha_pos ha_ne
       (hellingerDiv_smul_left_ne_top ha_pos ha_ne h c),
     toReal_hellingerDiv_eq_integral_of_ne_top ha_pos ha_ne h, integral_rpow_rnDeriv_smul_left,
-    Measure.smul_apply, ENNReal.toReal_smul, NNReal.smul_def, smul_eq_mul]
+    smul_apply, ENNReal.toReal_smul, NNReal.smul_def, smul_eq_mul]
   have : (1 - a)⁻¹ = -(a - 1)⁻¹ := by rw [← neg_sub a 1, inv_neg]
   rw [this]
   ring
diff --git a/Statlib/Divergence/Renyi/Basic.lean b/Statlib/Divergence/Renyi/Basic.lean
index 581fad3..e28b9ef 100644
--- a/Statlib/Divergence/Renyi/Basic.lean
+++ b/Statlib/Divergence/Renyi/Basic.lean
@@ -186,7 +186,7 @@ lemma renyiDiv_one_eq_top_iff [NeZero μ] [IsFiniteMeasure μ] [IsFiniteMeasure
     renyiDiv 1 μ ν = ∞ ↔ klDiv μ ν = ∞ := by
   rw [renyiDiv_one]
   rcases eq_or_ne ν 0 with rfl | hν
-  · simp only [Measure.coe_zero, Pi.zero_apply, ENNReal.inv_zero, smul_zero, klDiv_zero_right]
+  · simp only [FunLike.coe_zero, Pi.zero_apply, ENNReal.inv_zero, smul_zero, klDiv_zero_right]
   have : NeZero ν := ⟨hν⟩
   rw [klDiv_smul_right_eq_top_iff (ENNReal.inv_ne_zero.mpr (measure_ne_top _ _))
       (ENNReal.inv_ne_top.mpr (NeZero.ne _)),
@@ -358,7 +358,7 @@ lemma renyiDiv_zero_measure_left (ha_nonneg : 0 ≤ a) (ha : a ≠ 1) (ν : Meas
     rw [h_set, ENNReal.zero_div, ENNReal.log_zero, EReal.neg_bot, EReal.toENNReal_top]
   rw [renyiDiv_of_ne_one ha_zero ha]
   simp only [EReal.coe_add, EReal.coe_mul, EReal.coe_sub, EReal.coe_one, ne_eq, measure_ne_top,
-    not_false_eq_true, EReal.coe_ennreal_toReal, Measure.coe_zero, Pi.zero_apply,
+    not_false_eq_true, EReal.coe_ennreal_toReal, FunLike.coe_zero, Pi.zero_apply,
     ENNReal.toReal_zero, mul_zero, EReal.coe_zero, add_zero, log_zero, zero_add,
     hellingerDiv_zero_measure_left (ha_nonneg.lt_of_ne' ha_zero)]
   have : (1 - (a : EReal)) * (ν Set.univ) + (a - 1) * (ν Set.univ) = 0 := by
@@ -386,7 +386,7 @@ lemma renyiDiv_zero_measure_right (ha_nonneg : 0 ≤ a)
   have ha_pos : 0 < a := ha_nonneg.lt_of_ne' ha_zero
   rcases lt_trichotomy a 1 with (ha | rfl | ha)
   · rw [renyiDiv_of_ne_one ha_zero ha.ne, hellingerDiv_zero_measure_right_of_lt_one ha_pos ha]
-    simp only [EReal.coe_add, Measure.coe_zero, Pi.zero_apply, ENNReal.toReal_zero, mul_zero,
+    simp only [EReal.coe_add, FunLike.coe_zero, Pi.zero_apply, ENNReal.toReal_zero, mul_zero,
       EReal.coe_zero, EReal.coe_mul, zero_add, EReal.coe_ennreal_mul, EReal.coe_ennreal_ofReal,
       EReal.toENNReal_eq_top_iff, log_zero, add_zero]
     have : (a : EReal) * (μ Set.univ).toReal + (a - 1) * ((max (a * (1 - a)⁻¹) 0) * (μ Set.univ))
@@ -407,10 +407,10 @@ lemma renyiDiv_zero_measure_right (ha_nonneg : 0 ≤ a)
     norm_cast
     exact EReal.coe_ne_top _
   · rw [renyiDiv_one]
-    simp only [Measure.coe_zero, Pi.zero_apply, ENNReal.inv_zero, smul_zero]
+    simp only [FunLike.coe_zero, Pi.zero_apply, ENNReal.inv_zero, smul_zero]
     exact klDiv_zero_right
   · rw [renyiDiv_of_ne_one ha_zero ha.ne', hellingerDiv_zero_measure_right_of_one_le ha.le]
-    simp only [EReal.coe_add, Measure.coe_zero, Pi.zero_apply, ENNReal.toReal_zero, mul_zero,
+    simp only [EReal.coe_add, FunLike.coe_zero, Pi.zero_apply, ENNReal.toReal_zero, mul_zero,
       EReal.coe_zero, EReal.coe_mul, zero_add, EReal.coe_ennreal_top, EReal.toENNReal_eq_top_iff,
       log_zero, add_zero]
     have : ((a : EReal) - 1) * ⊤ = ⊤ := by
@@ -837,7 +837,7 @@ lemma renyiDiv_eq_renyiDiv_inv_smul (ha_nonneg : 0 ≤ a) [IsFiniteMeasure μ] [
   rcases eq_zero_or_neZero μ with rfl | _
   · have := ν.smul_finite (ENNReal.inv_ne_top.mpr (NeZero.ne (ν .univ)))
     rcases eq_or_ne a 1 with rfl | ha1
-    · simp [renyiDiv_one]
+    · simp [renyiDiv_one, ENNReal.inv_mul_cancel (NeZero.ne (ν .univ)) (measure_ne_top _ _)]
     · simp only [smul_zero, renyiDiv_zero_measure_left ha_nonneg ha1]
   exact (renyiDiv_smul_smul ha_nonneg (ENNReal.inv_ne_zero.mpr (measure_ne_top _ _))
     (ENNReal.inv_ne_top.mpr (NeZero.ne _)) (ENNReal.inv_ne_zero.mpr (measure_ne_top _ _))
diff --git a/Statlib/Divergence/Renyi/ProdCountable.lean b/Statlib/Divergence/Renyi/ProdCountable.lean
index f7a08c2..a50f3c3 100644
--- a/Statlib/Divergence/Renyi/ProdCountable.lean
+++ b/Statlib/Divergence/Renyi/ProdCountable.lean
@@ -90,7 +90,7 @@ theorem tendsto_renyiDiv_map_of_iSup_comap_eq (ha : 0 < a) (μ ν : Measure α)
     refine tendsto_const_nhds.congr fun n ↦ ?_
     rw [Measure.map_zero]
     rcases eq_or_ne a 1 with rfl | ha1
-    · simp_rw [renyiDiv_one, Measure.coe_zero, Pi.zero_apply, smul_zero,
+    · simp_rw [renyiDiv_one, FunLike.coe_zero, Pi.zero_apply, smul_zero,
         InformationTheory.klDiv_of_ac_of_integrable (.zero _) integrable_zero_measure]
       simp [measureReal_def, Measure.map_apply (hg n) .univ]
     · simp [renyiDiv_zero_measure_left ha.le ha1]
diff --git a/Statlib/Divergence/StatInfo/Basic.lean b/Statlib/Divergence/StatInfo/Basic.lean
index ffe1ba6..09be312 100644
--- a/Statlib/Divergence/StatInfo/Basic.lean
+++ b/Statlib/Divergence/StatInfo/Basic.lean
@@ -86,7 +86,7 @@ finite factor scales the statistical information by the same factor. -/
 lemma statInfo_smul_prior (μ ν : Measure 𝒳) (π : Measure Bool) {c : ℝ≥0∞} (hc : c ≠ ∞) :
     statInfo μ ν (c • π) = c * statInfo μ ν π := by
   rw [statInfo_eq_min_sub, statInfo_eq_min_sub, bayesBinaryRisk_smul_prior μ ν π hc,
-    Measure.smul_apply, Measure.smul_apply, smul_eq_mul, smul_eq_mul, mul_assoc, mul_assoc,
+    smul_apply, smul_apply, smul_eq_mul, smul_eq_mul, mul_assoc, mul_assoc,
     ← mul_min, ENNReal.mul_sub fun _ _ ↦ hc]
 
 @[simp] lemma statInfo_zero_left : statInfo 0 ν π = 0 := by simp [statInfo_eq_min_sub]
diff --git a/Statlib/Divergence/StatInfo/CurvatureMeasure.lean b/Statlib/Divergence/StatInfo/CurvatureMeasure.lean
index 7aa5fa4..9ade3c8 100644
--- a/Statlib/Divergence/StatInfo/CurvatureMeasure.lean
+++ b/Statlib/Divergence/StatInfo/CurvatureMeasure.lean
@@ -87,7 +87,7 @@ lemma measure_rightDerivStieltjes_statInfoDivFun (hβ : 0 < β) (hγ : 0 < γ) :
   -- the part of the measure on `Iic 0` is an infinite atom at `0`
   have h_Iic : g.measure.restrict (Iic 0) = ∞ • Measure.dirac 0 := by
     ext s hs
-    rw [Measure.restrict_apply hs, Measure.smul_apply, Measure.dirac_apply' _ hs, smul_eq_mul]
+    rw [Measure.restrict_apply hs, smul_apply, Measure.dirac_apply' _ hs, smul_eq_mul]
     by_cases h0 : (0 : ℝ) ∈ s
     · rw [indicator_of_mem h0, Pi.one_apply, mul_one]
       refine top_le_iff.mp ?_
@@ -112,7 +112,7 @@ lemma measure_rightDerivStieltjes_statInfoDivFun (hβ : 0 < β) (hγ : 0 < γ) :
     exact ENNReal.ofReal_lt_top⟩
   have h_Ioi : g.measure.restrict (Ioi 0) = ENNReal.ofReal β • Measure.dirac (γ / β) := by
     refine Measure.ext_of_Iic _ _ fun x ↦ ?_
-    rw [Measure.restrict_apply measurableSet_Iic, Iic_inter_Ioi, Measure.smul_apply,
+    rw [Measure.restrict_apply measurableSet_Iic, Iic_inter_Ioi, smul_apply,
       Measure.dirac_apply' _ measurableSet_Iic, smul_eq_mul]
     rcases le_or_gt x 0 with hx | hx
     · rw [Ioc_eq_empty (not_lt.mpr hx), measure_empty,
diff --git a/Statlib/Divergence/StatInfo/Event.lean b/Statlib/Divergence/StatInfo/Event.lean
index c3d7416..fbecacb 100644
--- a/Statlib/Divergence/StatInfo/Event.lean
+++ b/Statlib/Divergence/StatInfo/Event.lean
@@ -72,7 +72,7 @@ theorem statInfo_eq_iSup_sub (μ ν : Measure 𝒳) [IsFiniteMeasure μ] [IsFini
   have := μ.smul_finite (measure_ne_top π {false})
   have := ν.smul_finite (measure_ne_top π {true})
   rw [statInfo_eq_statInfo_one_one, statInfo_one_one_eq_iSup_sub_sub]
-  simp only [Measure.smul_apply, smul_eq_mul]
+  simp only [smul_apply, smul_eq_mul]
 
 /-- **Statistical information as a supremum over events**: for finite measures and a finite prior,
 `I_π(μ, ν) = sup_E (π₀ μ(E) - π₁ ν(E)) - max {0, π₀ μ(𝒳) - π₁ ν(𝒳)}`. -/
diff --git a/Statlib/Divergence/StatInfo/FDiv.lean b/Statlib/Divergence/StatInfo/FDiv.lean
index 1ef699c..2cd125c 100644
--- a/Statlib/Divergence/StatInfo/FDiv.lean
+++ b/Statlib/Divergence/StatInfo/FDiv.lean
@@ -176,7 +176,7 @@ private lemma integral_max_eq_integral_abs [IsFiniteMeasure μ] [IsFiniteMeasure
   swap; · exact (integrable_add_const_iff.mpr h_int).abs
   congr
   nth_rw 2 [μ.haveLebesgueDecomposition_add ν]
-  simp only [Measure.coe_add, Pi.add_apply, MeasurableSet.univ, withDensity_apply,
+  simp only [FunLike.coe_add, Pi.add_apply, MeasurableSet.univ, withDensity_apply,
     Measure.restrict_univ]
   rw [ENNReal.toReal_add (measure_ne_top _ _)]
   swap; · exact lt_top_iff_ne_top.mp <| (setLIntegral_univ _ ▸
@@ -201,7 +201,7 @@ private lemma integral_max_eq_integral_abs' [IsFiniteMeasure μ] [IsFiniteMeasur
   swap; · exact (h_int.sub (integrable_const _)).abs
   congr
   nth_rw 2 [μ.haveLebesgueDecomposition_add ν]
-  simp only [Measure.coe_add, Pi.add_apply, MeasurableSet.univ, withDensity_apply,
+  simp only [FunLike.coe_add, Pi.add_apply, MeasurableSet.univ, withDensity_apply,
     Measure.restrict_univ]
   rw [ENNReal.toReal_add (measure_ne_top _ _)]
   swap; · exact lt_top_iff_ne_top.mp <| (setLIntegral_univ _ ▸
diff --git a/Statlib/ForMathlib/InformationTheory/KullbackLeibler/Basic.lean b/Statlib/ForMathlib/InformationTheory/KullbackLeibler/Basic.lean
index 066d820..7a4e3fb 100644
--- a/Statlib/ForMathlib/InformationTheory/KullbackLeibler/Basic.lean
+++ b/Statlib/ForMathlib/InformationTheory/KullbackLeibler/Basic.lean
@@ -174,7 +174,7 @@ lemma klDiv_inv_smul_le_of_le {β : Type*} {mβ : MeasurableSpace β} {μ₁ ν
   · have hν₁ : ν₁ .univ = 0 := h_eq_ν.trans hν
     obtain rfl := Measure.measure_univ_eq_zero.mp hν
     obtain rfl := Measure.measure_univ_eq_zero.mp hν₁
-    simp only [Measure.coe_zero, Pi.zero_apply, ENNReal.inv_zero, smul_zero]
+    simp only [FunLike.coe_zero, Pi.zero_apply, ENNReal.inv_zero, smul_zero]
     by_cases hμ : μ₂ = 0
     · subst hμ
       obtain rfl : μ₁ = 0 := Measure.measure_univ_eq_zero.mp (h_eq_μ.trans (by simp))
diff --git a/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean b/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean
index 099604e..820be6b 100644
--- a/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean
+++ b/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean
@@ -86,7 +86,7 @@ lemma singularPart_eq_restrict_rnDeriv_add_eq_zero (μ ν : Measure α) [SigmaFi
     exact hxN.2 (hx hxN.1)
   refine singularPart_eq_restrict ?_ hνN
   rw [← restrict_apply_univ, ← singularPart_restrict μ ν hN.compl, singularPart_eq_zero_of_ac h_ac,
-    coe_zero, Pi.zero_apply]
+    FunLike.coe_zero, Pi.zero_apply]
 
 /-- On the set where `∂μ/∂ν` does not vanish, `∂ν/∂μ` is its inverse, `ν`-almost everywhere. -/
 lemma rnDeriv_eq_inv_rnDeriv_of_ne_zero (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
diff --git a/Statlib/ForMathlib/MeasureTheory/Measure/ERealStieltjes.lean b/Statlib/ForMathlib/MeasureTheory/Measure/ERealStieltjes.lean
index 8b87331..12c9e44 100644
--- a/Statlib/ForMathlib/MeasureTheory/Measure/ERealStieltjes.lean
+++ b/Statlib/ForMathlib/MeasureTheory/Measure/ERealStieltjes.lean
@@ -1447,9 +1447,9 @@ lemma measure_add (f g : ERealStieltjes) :
       rw [measure_Ioc_add hab.le hfp hfq hgp hgq]
       exact ENNReal.add_ne_top.mpr ⟨f.measure_Ioc_ne_top hfp hfq, g.measure_Ioc_ne_top hgp hgq⟩
     refine Measure.ext_of_Ioc_finite _ _ ?_ fun x y hxy ↦ ?_
-    · simp only [Measure.restrict_apply_univ, Measure.coe_add, Pi.add_apply]
+    · simp only [Measure.restrict_apply_univ, FunLike.coe_add, Pi.add_apply]
       exact measure_Ioc_add hab.le hfp hfq hgp hgq
-    · simp only [Measure.restrict_apply measurableSet_Ioc, Measure.coe_add, Pi.add_apply,
+    · simp only [Measure.restrict_apply measurableSet_Ioc, FunLike.coe_add, Pi.add_apply,
         Ioc_inter_Ioc]
       rcases le_or_gt (min y b) (max x a) with h | h
       · simp [Ioc_eq_empty_of_le h]
@@ -1460,7 +1460,7 @@ lemma measure_add (f g : ERealStieltjes) :
   · -- at the two jump points, both measures have an infinite atom
     rw [Measure.restrict_singleton, Measure.restrict_singleton]
     congr 1
-    rw [Measure.coe_add, Pi.add_apply]
+    rw [FunLike.coe_add, Pi.add_apply]
     rcases hx with hx | hx
     · rw [φ.measure_singleton_eq_top fun y hy ↦ by rw [hx.2 y hy, EReal.sub_bot hx.1.1],
         eq_comm, ENNReal.add_eq_top]
@@ -1513,7 +1513,7 @@ lemma measure_add_of_eq_bot_iff_of_eq_top_iff (f g : ERealStieltjes)
       rcases add_apply_eq_top_iff.mp hy with h | h
       exacts [⟨h, (h_top y).mp h⟩, ⟨(h_top y).mpr h, h⟩]
   rw [measure_add, Measure.restrict_eq_self_of_ae_mem]
-  rw [ae_iff, Measure.coe_add, Pi.add_apply, add_eq_zero]
+  rw [ae_iff, FunLike.coe_add, Pi.add_apply, add_eq_zero]
   constructor
   · refine measure_mono_null (fun x hx ↦ ?_)
       (measure_union_null f.measure_setOf_eq_bot f.measure_setOf_exists_lt_eq_top)
diff --git a/Statlib/ForMathlib/Probability/Decision/ZeroOneLoss.lean b/Statlib/ForMathlib/Probability/Decision/ZeroOneLoss.lean
index 48e1c33..ec632cb 100644
--- a/Statlib/ForMathlib/Probability/Decision/ZeroOneLoss.lean
+++ b/Statlib/ForMathlib/Probability/Decision/ZeroOneLoss.lean
@@ -91,7 +91,7 @@ lemma map_uncurry_compProd_of_mem_zero_one (hℓ : Measurable (uncurry ℓ))
   set A := {p : Θ × 𝓨 | ℓ p.1 p.2 = 1}
   have hA : MeasurableSet A := hℓ (measurableSet_singleton 1)
   ext s hs
-  rw [Measure.map_apply hℓ hs, Measure.add_apply, Measure.smul_apply, Measure.smul_apply,
+  rw [Measure.map_apply hℓ hs, add_apply, smul_apply, smul_apply,
     Measure.dirac_apply' _ hs, Measure.dirac_apply' _ hs, smul_eq_mul, smul_eq_mul]
   have h_pre : uncurry ℓ ⁻¹' s
       = (if (0 : ℝ≥0∞) ∈ s then Aᶜ else ∅) ∪ (if (1 : ℝ≥0∞) ∈ s then A else ∅) := by
diff --git a/Statlib/ForMathlib/Probability/Distributions/Bernoulli.lean b/Statlib/ForMathlib/Probability/Distributions/Bernoulli.lean
index 6b5b9e8..4f52d21 100644
--- a/Statlib/ForMathlib/Probability/Distributions/Bernoulli.lean
+++ b/Statlib/ForMathlib/Probability/Distributions/Bernoulli.lean
@@ -233,7 +233,7 @@ lemma bernoulliKernel_comp_eq_bernoulliMeasure (x y : 𝓧) (μ : Measure I) [Is
     simp
   ext s hs
   rw [Measure.bind_apply hs (bernoulliKernel x y).aemeasurable]
-  simp_rw [bernoulliKernel_apply, bernoulliMeasure_def, Measure.add_apply, Measure.smul_apply,
+  simp_rw [bernoulliKernel_apply, bernoulliMeasure_def, add_apply, smul_apply,
     ENNReal.smul_def, smul_eq_mul, coe_toNNReal_eq_ofReal, coe_symm_eq]
   rw [lintegral_add_left (by fun_prop), lintegral_mul_const _ (by fun_prop),
     lintegral_mul_const _ (by fun_prop), h1, h2]
diff --git a/Statlib/ForMathlib/Probability/Kernel/Composition/MeasureCompProd.lean b/Statlib/ForMathlib/Probability/Kernel/Composition/MeasureCompProd.lean
index a1bb2db..f1181cb 100644
--- a/Statlib/ForMathlib/Probability/Kernel/Composition/MeasureCompProd.lean
+++ b/Statlib/ForMathlib/Probability/Kernel/Composition/MeasureCompProd.lean
@@ -338,7 +338,7 @@ instance _root_.MeasureTheory.Measure.neZero_compProd [SFinite μ] [NeZero μ] [
     NeZero (μ ⊗ₘ κ) :=
   ⟨fun h ↦ NeZero.ne μ (by
     rw [← Measure.measure_univ_eq_zero, ← Measure.compProd_apply_univ (κ := κ), h,
-      Measure.coe_zero, Pi.zero_apply])⟩
+      FunLike.coe_zero, Pi.zero_apply])⟩
 
 end CompProd
 
diff --git a/Statlib/Testing/Binary.lean b/Statlib/Testing/Binary.lean
index 5a1cbb9..a0bd427 100644
--- a/Statlib/Testing/Binary.lean
+++ b/Statlib/Testing/Binary.lean
@@ -325,7 +325,7 @@ lemma bayesBinaryRisk_eq_lintegral_min_rnDeriv (μ ν : Measure 𝒳) [IsFiniteM
       ⟨h.nullSet, h.measurableSet_nullSet, h.measure_nullSet, h.measure_compl_nullSet⟩
     have h_false : μ (F ∩ t) ≤ ∫⁻ x in F, (∂μ/∂ν) x ∂ν := by
       conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
-      rw [Measure.add_apply, withDensity_apply _ (hF.inter ht),
+      rw [add_apply, withDensity_apply _ (hF.inter ht),
         measure_mono_null Set.inter_subset_right hμt, zero_add]
       exact lintegral_mono_set Set.inter_subset_left
     have h_true : ν (F ∩ t)ᶜ ≤ ν Fᶜ := by
@@ -444,7 +444,7 @@ lemma toReal_bayesBinaryRisk_eq_integral_abs (μ ν : Measure 𝒳) [IsFiniteMea
         (absolutelyContinuous_boolKernel_comp_right μ ν hπ_true)]
       rw [measureReal_def]
     _ = _ := by
-      simp_rw [add_comm, Measure.coe_add, Measure.coe_smul, Pi.add_apply, Pi.smul_apply,
+      simp_rw [add_comm, FunLike.coe_add, FunLike.coe_smul, Pi.add_apply, Pi.smul_apply,
         smul_eq_mul, ENNReal.toReal_add (ENNReal.mul_ne_top (measure_ne_top _ _)
         (measure_ne_top _ _)) (ENNReal.mul_ne_top (measure_ne_top _ _) (measure_ne_top _ _)),
         ENNReal.toReal_mul]