-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma withDensity_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x)) = κ

Proof state:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ↑(κ.rnDerivAux (κ + η) a b).toNNReal ∂(κ + η) a = (κ a) s

case h.h.hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ Measurable (Function.uncurry fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal)

Tactic:
swap

Result:
case h.h.hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ Measurable (Function.uncurry fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal)

case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ↑(κ.rnDerivAux (κ + η) a b).toNNReal ∂(κ + η) a = (κ a) s

Proof state:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ (((κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) a) s = (κ a) s

Tactic:
rw [Kernel.withDensity_apply']

Result:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ↑(κ.rnDerivAux (κ + η) a b).toNNReal ∂(κ + η) a = (κ a) s

case h.h.hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ Measurable (Function.uncurry fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal)

Proof state:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ↑(κ.rnDerivAux (κ + η) a b).toNNReal ∂(κ + η) a = (κ a) s

Tactic:
simp_rw [ofNNReal_toNNReal]

Result:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) ∂(κ + η) a = (κ a) s

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ ((κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) = κ

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ (((κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) a) s = (κ a) s

Proof state:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) ∂(κ + η) a = (κ a) s

Tactic:
exact setLIntegral_rnDerivAux κ η a hs

Result:
no goals

Proof state:
case h.h.hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ Measurable (Function.uncurry fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal)

Tactic:
fun_prop

Result:
no goals