chore(Probability/Kernel): add fun_prop attributes, use it (#21861)

I marked measurability lemmas about kernels with `fun_prop` and used that tactic in various places to replace measurability proofs.

Using `fun_prop` instead of manual proofs improved some proofs and allowed removing several now unused typeclass arguments.

Author: RemyDegenne

Mathlib/MeasureTheory/Measure/GiryMonad.lean

@@ -85,17 +85,20 @@ theorem _root_.Measurable.measure_of_isPiSystem_of_isProbabilityMeasure {μ : α
     (h_basic : ∀ s ∈ S, Measurable fun a ↦ μ a s) : Measurable μ :=
   .measure_of_isPiSystem hgen hpi h_basic <| by simp
 
+@[fun_prop]
 theorem measurable_map (f : α → β) (hf : Measurable f) :
     Measurable fun μ : Measure α => map f μ := by
   refine measurable_of_measurable_coe _ fun s hs => ?_
   simp_rw [map_apply hf hs]
   exact measurable_coe (hf hs)
 
+@[fun_prop]
 theorem measurable_dirac : Measurable (Measure.dirac : α → Measure α) := by
   refine measurable_of_measurable_coe _ fun s hs => ?_
   simp_rw [dirac_apply' _ hs]
   exact measurable_one.indicator hs
 
+@[fun_prop]
 theorem measurable_lintegral {f : α → ℝ≥0∞} (hf : Measurable f) :
     Measurable fun μ : Measure α => ∫⁻ x, f x ∂μ := by
   simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]
@@ -124,6 +127,7 @@ theorem join_zero : (0 : Measure (Measure α)).join = 0 := by
   ext1 s hs
   simp only [hs, join_apply, lintegral_zero_measure, coe_zero, Pi.zero_apply]
 
+@[fun_prop]
 theorem measurable_join : Measurable (join : Measure (Measure α) → Measure α) :=
   measurable_of_measurable_coe _ fun s hs => by
     simp only [join_apply hs]; exact measurable_lintegral (measurable_coe hs)
@@ -144,7 +148,7 @@ theorem lintegral_join {m : Measure (Measure α)} {f : α → ℝ≥0∞} (hf :
   intro s f hf hm
   rw [lintegral_iSup _ hm]
   swap
-  · exact fun n => Finset.measurable_sum _ fun r _ => (hf _ _).const_mul _
+  · fun_prop
   congr
   funext n
   rw [lintegral_finset_sum (s n)]
@@ -180,6 +184,7 @@ lemma bind_const {m : Measure α} {ν : Measure β} : m.bind (fun _ ↦ ν) = m
   ext s hs
   rw [bind_apply hs measurable_const, lintegral_const, smul_apply, smul_eq_mul, mul_comm]
 
+@[fun_prop]
 theorem measurable_bind' {g : α → Measure β} (hg : Measurable g) : Measurable fun m => bind m g :=
   measurable_join.comp (measurable_map _ hg)
 
@@ -211,7 +216,7 @@ lemma bind_dirac_eq_map (m : Measure α) {f : α → β} (hf : Measurable f) :
     m.bind (fun x ↦ Measure.dirac (f x)) = m.map f := by
   ext s hs
   rw [bind_apply hs]
-  swap; · exact measurable_dirac.comp hf
+  swap; · fun_prop
   simp_rw [dirac_apply' _ hs]
   rw [← lintegral_map _ hf, lintegral_indicator_one hs]
   exact measurable_const.indicator hs

Mathlib/Probability/Kernel/Composition/Basic.lean

@@ -118,7 +118,7 @@ theorem compProdFun_iUnion (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSF
   · simp [compProdFun]
   · intro i
     have hm : MeasurableSet {p : (α × β) × γ | (p.1.2, p.2) ∈ f i} :=
-      measurable_fst.snd.prod_mk measurable_snd (hf_meas i)
+      (hf_meas i).preimage (by fun_prop)
     exact ((measurable_kernel_prod_mk_left hm).comp measurable_prod_mk_left).aemeasurable
 
 theorem compProdFun_tsum_right (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α)
@@ -401,9 +401,7 @@ theorem lintegral_compProd' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kerne
         (fun ab => ∫⁻ c, f' (ab.2, c) ∂η ab) ∘ fun b => (a, b) := by
       ext1 ab; rfl
     rw [this]
-    apply Measurable.comp _ (measurable_prod_mk_left (m := mα))
-    exact Measurable.lintegral_kernel_prod_right
-      ((SimpleFunc.measurable _).comp (measurable_fst.snd.prod_mk measurable_snd))
+    fun_prop
   rw [lintegral_iSup]
   rotate_left
   · exact fun n => h_some_meas_integral (F n)
@@ -588,7 +586,7 @@ use `map κ f` instead. -/
 noncomputable def mapOfMeasurable (κ : Kernel α β) (f : β → γ) (hf : Measurable f) :
     Kernel α γ where
   toFun a := (κ a).map f
-  measurable' := (Measure.measurable_map _ hf).comp (Kernel.measurable κ)
+  measurable' := by fun_prop
 
 open Classical in
 /-- The pushforward of a kernel along a function.
@@ -1201,7 +1199,7 @@ instance IsSFiniteKernel.comp (η : Kernel β γ) [IsSFiniteKernel η] (κ : Ker
     [IsSFiniteKernel κ] : IsSFiniteKernel (η ∘ₖ κ) := by rw [comp_eq_snd_compProd]; infer_instance
 
 /-- Composition of kernels is associative. -/
-theorem comp_assoc {δ : Type*} {mδ : MeasurableSpace δ} (ξ : Kernel γ δ) [IsSFiniteKernel ξ]
+theorem comp_assoc {δ : Type*} {mδ : MeasurableSpace δ} (ξ : Kernel γ δ)
     (η : Kernel β γ) (κ : Kernel α β) : ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ) := by
   refine ext_fun fun a f hf => ?_
   simp_rw [lintegral_comp _ _ _ hf, lintegral_comp _ _ _ hf.lintegral_kernel]
@@ -1351,20 +1349,20 @@ lemma comap_prod_swap (κ : Kernel α β) (η : Kernel γ δ) [IsSFiniteKernel 
   intro x f hf
   rw [lintegral_comap, lintegral_map _ measurable_swap _ hf, lintegral_prod _ _ _ hf,
     lintegral_prod]
-  swap; · exact hf.comp measurable_swap
+  swap; · fun_prop
   simp only [prodMkRight_apply, Prod.fst_swap, Prod.swap_prod_mk, lintegral_prodMkLeft,
     Prod.snd_swap]
   refine (lintegral_lintegral_swap ?_).symm
-  exact (hf.comp measurable_swap).aemeasurable
+  fun_prop
 
 lemma map_prod_swap (κ : Kernel α β) (η : Kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
     map (κ ×ₖ η) Prod.swap = η ×ₖ κ := by
   rw [ext_fun_iff]
   intro x f hf
   rw [lintegral_map _ measurable_swap _ hf, lintegral_prod, lintegral_prod _ _ _ hf]
-  swap; · exact hf.comp measurable_swap
+  swap; · fun_prop
   refine (lintegral_lintegral_swap ?_).symm
-  exact hf.aemeasurable
+  fun_prop
 
 @[simp]
 lemma swap_prod {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel α γ} [IsSFiniteKernel η] :

Mathlib/Probability/Kernel/Defs.lean

@@ -73,7 +73,9 @@ instance instFunLike : FunLike (Kernel α β) α (Measure β) where
   coe := toFun
   coe_injective' f g h := by cases f; cases g; congr
 
+@[fun_prop]
 lemma measurable (κ : Kernel α β) : Measurable κ := κ.measurable'
+
 @[simp, norm_cast] lemma coe_mk (f : α → Measure β) (hf) : mk f hf = f := rfl
 
 initialize_simps_projections Kernel (toFun → apply)

Mathlib/Probability/Kernel/Invariance.lean

@@ -75,7 +75,7 @@ theorem Invariant.def (hκ : Invariant κ μ) : μ.bind κ = μ :=
 theorem Invariant.comp_const (hκ : Invariant κ μ) : κ ∘ₖ const α μ = const α μ := by
   rw [← const_bind_eq_comp_const κ μ, hκ.def]
 
-theorem Invariant.comp [IsSFiniteKernel κ] (hκ : Invariant κ μ) (hη : Invariant η μ) :
+theorem Invariant.comp (hκ : Invariant κ μ) (hη : Invariant η μ) :
     Invariant (κ ∘ₖ η) μ := by
   cases' isEmpty_or_nonempty α with _ hα
   · exact Subsingleton.elim _ _

Mathlib/Probability/Kernel/MeasurableLIntegral.lean

@@ -118,6 +118,7 @@ theorem Kernel.measurable_lintegral_indicator_const {t : Set (α × β)} (ht : M
 /-- For an s-finite kernel `κ` and a function `f : α → β → ℝ≥0∞` which is measurable when seen as a
 map from `α × β` (hypothesis `Measurable (uncurry f)`), the integral `a ↦ ∫⁻ b, f a b ∂(κ a)` is
 measurable. -/
+@[fun_prop]
 theorem _root_.Measurable.lintegral_kernel_prod_right {f : α → β → ℝ≥0∞}
     (hf : Measurable (uncurry f)) : Measurable fun a => ∫⁻ b, f a b ∂κ a := by
   let F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
@@ -150,13 +151,11 @@ theorem _root_.Measurable.lintegral_kernel_prod_right {f : α → β → ℝ≥0
     rw [h_add]
     exact Measurable.add hm₁ hm₂
 
+@[fun_prop]
 theorem _root_.Measurable.lintegral_kernel_prod_right' {f : α × β → ℝ≥0∞} (hf : Measurable f) :
-    Measurable fun a => ∫⁻ b, f (a, b) ∂κ a := by
-  refine Measurable.lintegral_kernel_prod_right ?_
-  have : (uncurry fun (a : α) (b : β) => f (a, b)) = f := by
-    ext x; rw [uncurry_apply_pair]
-  rwa [this]
+    Measurable fun a => ∫⁻ b, f (a, b) ∂κ a := by fun_prop
 
+@[fun_prop]
 theorem _root_.Measurable.lintegral_kernel_prod_right'' {f : β × γ → ℝ≥0∞} (hf : Measurable f) :
     Measurable fun x => ∫⁻ y, f (x, y) ∂η (a, x) := by
   -- Porting note: used `Prod.mk a` instead of `fun x => (a, x)` below
@@ -166,35 +165,35 @@ theorem _root_.Measurable.lintegral_kernel_prod_right'' {f : β × γ → ℝ≥
   -- Porting note: specified `κ`, `f`.
   refine (Measurable.lintegral_kernel_prod_right' (κ := η)
     (f := (fun u ↦ f (u.fst.snd, u.snd))) ?_).comp measurable_prod_mk_left
-  exact hf.comp (measurable_fst.snd.prod_mk measurable_snd)
+  fun_prop
 
 theorem _root_.Measurable.setLIntegral_kernel_prod_right {f : α → β → ℝ≥0∞}
     (hf : Measurable (uncurry f)) {s : Set β} (hs : MeasurableSet s) :
     Measurable fun a => ∫⁻ b in s, f a b ∂κ a := by
-  simp_rw [← lintegral_restrict κ hs]; exact hf.lintegral_kernel_prod_right
+  simp_rw [← lintegral_restrict κ hs]; fun_prop
 
+@[fun_prop]
 theorem _root_.Measurable.lintegral_kernel_prod_left' {f : β × α → ℝ≥0∞} (hf : Measurable f) :
-    Measurable fun y => ∫⁻ x, f (x, y) ∂κ y :=
-  (measurable_swap_iff.mpr hf).lintegral_kernel_prod_right'
+    Measurable fun y => ∫⁻ x, f (x, y) ∂κ y := by fun_prop
 
+@[fun_prop]
 theorem _root_.Measurable.lintegral_kernel_prod_left {f : β → α → ℝ≥0∞}
-    (hf : Measurable (uncurry f)) : Measurable fun y => ∫⁻ x, f x y ∂κ y :=
-  hf.lintegral_kernel_prod_left'
+    (hf : Measurable (uncurry f)) : Measurable fun y => ∫⁻ x, f x y ∂κ y := by fun_prop
 
 theorem _root_.Measurable.setLIntegral_kernel_prod_left {f : β → α → ℝ≥0∞}
     (hf : Measurable (uncurry f)) {s : Set β} (hs : MeasurableSet s) :
     Measurable fun b => ∫⁻ a in s, f a b ∂κ b := by
-  simp_rw [← lintegral_restrict κ hs]; exact hf.lintegral_kernel_prod_left
+  simp_rw [← lintegral_restrict κ hs]; fun_prop
 
-theorem _root_.Measurable.lintegral_kernel {f : β → ℝ≥0∞} (hf : Measurable f) :
-    Measurable fun a => ∫⁻ b, f b ∂κ a :=
-  Measurable.lintegral_kernel_prod_right (hf.comp measurable_snd)
+@[fun_prop]
+theorem _root_.Measurable.lintegral_kernel {κ : Kernel α β} {f : β → ℝ≥0∞} (hf : Measurable f) :
+    Measurable fun a => ∫⁻ b, f b ∂κ a := by fun_prop
 
 theorem _root_.Measurable.setLIntegral_kernel {f : β → ℝ≥0∞} (hf : Measurable f) {s : Set β}
     (hs : MeasurableSet s) : Measurable fun a => ∫⁻ b in s, f b ∂κ a := by
   -- Porting note: was term mode proof (`Function.comp` reducibility)
   refine Measurable.setLIntegral_kernel_prod_right ?_ hs
-  convert hf.comp measurable_snd
+  fun_prop
 
 end Lintegral
 

Mathlib/Probability/Kernel/RadonNikodym.lean

@@ -107,6 +107,7 @@ lemma rnDerivAux_le_one [IsFiniteKernel η] (hκη : κ ≤ η) {a : α} :
   · have := hαγ.countableOrCountablyGenerated.resolve_left hα
     exact density_le_one ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _
 
+@[fun_prop]
 lemma measurable_rnDerivAux (κ η : Kernel α γ) :
     Measurable (fun p : α × γ ↦ Kernel.rnDerivAux κ η p.1 p.2) := by
   simp_rw [rnDerivAux]
@@ -124,10 +125,9 @@ lemma measurable_rnDerivAux (κ η : Kernel α γ) :
   · have := hαγ.countableOrCountablyGenerated.resolve_left hα
     exact measurable_density _ η MeasurableSet.univ
 
+@[fun_prop]
 lemma measurable_rnDerivAux_right (κ η : Kernel α γ) (a : α) :
-    Measurable (fun x : γ ↦ rnDerivAux κ η a x) := by
-  change Measurable ((fun p : α × γ ↦ rnDerivAux κ η p.1 p.2) ∘ (fun x ↦ (a, x)))
-  exact (measurable_rnDerivAux _ _).comp measurable_prod_mk_left
+    Measurable (fun x : γ ↦ rnDerivAux κ η a x) := by fun_prop
 
 lemma setLIntegral_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η]
     (a : α) {s : Set γ} (hs : MeasurableSet s) :
@@ -150,8 +150,7 @@ lemma withDensity_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFinit
     withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x)) = κ := by
   ext a s hs
   rw [Kernel.withDensity_apply']
-  swap
-  · exact (measurable_rnDerivAux _ _).ennreal_ofReal
+  swap; · fun_prop
   simp_rw [ofNNReal_toNNReal]
   exact setLIntegral_rnDerivAux κ η a hs
 
@@ -174,7 +173,7 @@ lemma withDensity_one_sub_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ]
   rw [withDensity_sub_add_cancel]
   · rw [withDensity_one']
   · exact measurable_const
-  · exact (measurable_rnDerivAux _ _).ennreal_ofReal
+  · fun_prop
   · intro a
     filter_upwards [rnDerivAux_le_one h_le] with x hx
     simp only [ENNReal.ofReal_le_one]
@@ -217,12 +216,9 @@ lemma measure_mutuallySingularSetSlice (κ η : Kernel α γ) [IsFiniteKernel κ
   simp_rw [ofNNReal_toNNReal]
   rw [Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]
   rotate_left
-  · exact (measurable_const.sub
-      ((measurable_rnDerivAux _ _).comp measurable_prod_mk_left)).ennreal_ofReal
-      (measurableSet_singleton _)
-  · exact (measurable_const.sub
-      ((measurable_rnDerivAux _ _).comp measurable_prod_mk_left)).ennreal_ofReal
-  · exact (measurable_const.sub (measurable_rnDerivAux _ _)).ennreal_ofReal
+  · exact (measurableSet_singleton 0).preimage (by fun_prop)
+  · fun_prop
+  · fun_prop
   refine ae_of_all _ (fun x hx ↦ ?_)
   simp only [mem_setOf_eq] at hx
   simp [hx]
@@ -236,16 +232,16 @@ lemma rnDeriv_def' (κ η : Kernel α γ) :
     rnDeriv κ η = fun a x ↦ ENNReal.ofReal (rnDerivAux κ (κ + η) a x)
       / ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a x) := by ext; rw [rnDeriv_def]
 
+@[fun_prop]
 lemma measurable_rnDeriv (κ η : Kernel α γ) :
     Measurable (fun p : α × γ ↦ rnDeriv κ η p.1 p.2) := by
   simp_rw [rnDeriv_def]
   exact (measurable_rnDerivAux κ _).ennreal_ofReal.div
     (measurable_const.sub (measurable_rnDerivAux κ _)).ennreal_ofReal
 
+@[fun_prop]
 lemma measurable_rnDeriv_right (κ η : Kernel α γ) (a : α) :
-    Measurable (fun x : γ ↦ rnDeriv κ η a x) := by
-  change Measurable ((fun p : α × γ ↦ rnDeriv κ η p.1 p.2) ∘ (fun x ↦ (a, x)))
-  exact (measurable_rnDeriv _ _).comp measurable_prod_mk_left
+    Measurable (fun x : γ ↦ rnDeriv κ η a x) := by fun_prop
 
 lemma rnDeriv_eq_top_iff (κ η : Kernel α γ) (a : α) (x : γ) :
     rnDeriv κ η a x = ∞ ↔ (a, x) ∈ mutuallySingularSet κ η := by
@@ -267,9 +263,7 @@ irreducible_def singularPart (κ η : Kernel α γ) [IsSFiniteKernel κ] [IsSFin
 
 lemma measurable_singularPart_fun (κ η : Kernel α γ) :
     Measurable (fun p : α × γ ↦ Real.toNNReal (rnDerivAux κ (κ + η) p.1 p.2)
-      - Real.toNNReal (1 - rnDerivAux κ (κ + η) p.1 p.2) * rnDeriv κ η p.1 p.2) :=
-  (measurable_rnDerivAux _ _).ennreal_ofReal.sub
-    ((measurable_const.sub (measurable_rnDerivAux _ _)).ennreal_ofReal.mul (measurable_rnDeriv _ _))
+      - Real.toNNReal (1 - rnDerivAux κ (κ + η) p.1 p.2) * rnDeriv κ η p.1 p.2) := by fun_prop
 
 lemma measurable_singularPart_fun_right (κ η : Kernel α γ) (a : α) :
     Measurable (fun x : γ ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x)
@@ -351,9 +345,8 @@ lemma withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice
     exact (withDensity_one_sub_rnDerivAux κ η).symm
   rw [this, ← withDensity_mul, Kernel.withDensity_apply']
   rotate_left
-  · exact ((measurable_const.sub (measurable_rnDerivAux _ _)).ennreal_ofReal.mul
-    (measurable_rnDeriv _ _))
-  · exact (measurable_const.sub (measurable_rnDerivAux _ _)).real_toNNReal
+  · fun_prop
+  · fun_prop
   · exact measurable_rnDeriv _ _
   simp_rw [rnDeriv]
   have hs' : ∀ x ∈ s, rnDerivAux κ (κ + η) a x < 1 := by

Mathlib/Probability/Kernel/WithDensity.lean

@@ -111,8 +111,8 @@ theorem integral_withDensity {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ
     (hg : Measurable (Function.uncurry g)) :
     ∫ b, f b ∂withDensity κ (fun a b => g a b) a = ∫ b, g a b • f b ∂κ a := by
   rw [Kernel.withDensity_apply, integral_withDensity_eq_integral_smul]
-  · exact Measurable.of_uncurry_left hg
-  · exact measurable_coe_nnreal_ennreal.comp hg
+  · fun_prop
+  · fun_prop
 
 theorem withDensity_add_left (κ η : Kernel α β) [IsSFiniteKernel κ] [IsSFiniteKernel η]
     (f : α → β → ℝ≥0∞) : withDensity (κ + η) f = withDensity κ f + withDensity η f := by
@@ -139,7 +139,7 @@ lemma withDensity_add_right [IsSFiniteKernel κ] {f g : α → β → ℝ≥0∞
   ext a
   rw [coe_add, Pi.add_apply, Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg,
     Kernel.withDensity_apply, Pi.add_apply, MeasureTheory.withDensity_add_right]
-  · exact hg.comp measurable_prod_mk_left
+  · fun_prop
   · exact hf.add hg
 
 lemma withDensity_sub_add_cancel [IsSFiniteKernel κ] {f g : α → β → ℝ≥0∞}
@@ -166,11 +166,11 @@ theorem withDensity_tsum [Countable ι] (κ : Kernel α β) [IsSFiniteKernel κ]
       rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]
       exact Pi.summable.mpr fun p => ENNReal.summable
     rw [this]
-    exact Measurable.ennreal_tsum' hf
+    fun_prop
   have : ∫⁻ b in s, (∑' n, f n) a b ∂κ a = ∫⁻ b in s, ∑' n, (fun b => f n a b) b ∂κ a := by
     congr with b
     rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]
-  rw [this, lintegral_tsum fun n => (Measurable.of_uncurry_left (hf n)).aemeasurable]
+  rw [this, lintegral_tsum fun n => by fun_prop]
   congr with n
   rw [Kernel.withDensity_apply' _ (hf n) a s]
 
@@ -238,7 +238,7 @@ theorem isSFiniteKernel_withDensity_of_isFiniteKernel (κ : Kernel α β) [IsFin
     rw [Filter.EventuallyEq, Filter.eventually_atTop]
     exact ⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩
   rw [hf_eq_tsum, withDensity_tsum _ fun n : ℕ => _]
-  swap; · exact fun _ => (hf.min measurable_const).sub (hf.min measurable_const)
+  swap; · fun_prop
   refine isSFiniteKernel_sum (hκs := fun n => ?_)
   suffices IsFiniteKernel (withDensity κ (fs n)) by haveI := this; infer_instance
   refine isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b => ?_
@@ -273,14 +273,13 @@ nonrec lemma withDensity_mul [IsSFiniteKernel κ] {f : α → β → ℝ≥0} {g
       = withDensity (withDensity κ fun a x ↦ f a x) g := by
   ext a : 1
   rw [Kernel.withDensity_apply]
-  swap; · exact (measurable_coe_nnreal_ennreal.comp hf).mul hg
+  swap; · fun_prop
   change (Measure.withDensity (κ a) ((fun x ↦ (f a x : ℝ≥0∞)) * (fun x ↦ (g a x : ℝ≥0∞)))) =
       (withDensity (withDensity κ fun a x ↦ f a x) g) a
   rw [withDensity_mul]
   · rw [Kernel.withDensity_apply _ hg, Kernel.withDensity_apply]
     exact measurable_coe_nnreal_ennreal.comp hf
-  · rw [measurable_coe_nnreal_ennreal_iff]
-    exact hf.comp measurable_prod_mk_left
-  · exact hg.comp measurable_prod_mk_left
+  · fun_prop
+  · fun_prop
 
 end ProbabilityTheory.Kernel