-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_withDensity [IsFiniteKernel κ] {f : α → γ → ℝ≥0∞} [IsFiniteKernel (withDensity κ f)]
    (hf : Measurable (Function.uncurry f)) (a : α) :
    (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] ∂(κ.withDensity f) a/∂κ a
hf' : ∀ (a : α), Measurable (f a)
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] f a

Tactic:
filter_upwards [h_ae, (κ a).rnDeriv_withDensity (hf' a)] with x hx1 hx2

Result:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] ∂(κ.withDensity f) a/∂κ a
hf' : ∀ (a : α), Measurable (f a)
x : γ
hx1 : (κ.withDensity f).rnDeriv κ a x = (∂(κ.withDensity f) a/∂κ a) x
hx2 : (∂(κ a).withDensity (f a)/∂κ a) x = f a x
⊢ (κ.withDensity f).rnDeriv κ a x = f a x

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] ∂(κ.withDensity f) a/∂κ a
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] f a

Tactic:
have hf' : ∀ a, Measurable (f a) := fun _ ↦ hf.of_uncurry_left

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] ∂(κ.withDensity f) a/∂κ a
hf' : ∀ (a : α), Measurable (f a)
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] f a

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] f a

Tactic:
have h_ae := (κ.withDensity f).rnDeriv_eq_rnDeriv_measure (η := κ) (a := a)

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] ∂(κ.withDensity f) a/∂κ a
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] f a

Proof state:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᶠ[ae (κ a)] ∂(κ.withDensity f) a/∂κ a
hf' : ∀ (a : α), Measurable (f a)
x : γ
hx1 : (κ.withDensity f).rnDeriv κ a x = (∂(κ.withDensity f) a/∂κ a) x
hx2 : (∂(κ a).withDensity (f a)/∂κ a) x = f a x
⊢ (κ.withDensity f).rnDeriv κ a x = f a x

Tactic:
rw [hx1, κ.withDensity_apply hf, hx2]

Result:
no goals