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

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

Tactic:
have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le

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

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

Tactic:
have : ∀ b, (Real.toNNReal b : ℝ≥0∞) = ENNReal.ofReal b := fun _ ↦ rfl

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
⊢ (((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η

Proof state:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ≤ 1

Tactic:
simp only [ENNReal.ofReal_le_one]

Result:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
⊢ κ.rnDerivAux (κ + η) a x ≤ 1

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

Tactic:
simp only [coe_add, Pi.add_apply, Measure.coe_add] at h

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

Proof state:
case hfg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
a : α
⊢ (fun x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᶠ[ae ((κ + η) a)] fun x => 1

Tactic:
filter_upwards [rnDerivAux_le_one h_le] with x hx

Result:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ≤ 1

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

Tactic:
have h : (withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
      + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))) a s
    = κ a s + η a s := by
  rw [this]
  simp

Result:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η
a : α
s : Set γ
a✝ : MeasurableSet s
h :
  ((((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
          (κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal)
        a)
      s =
    (κ a) s + (η a) s
⊢ (((κ + η).withDensity fun a x => ↑(1 - κ.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 η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η
a : α
s : Set γ
a✝ : MeasurableSet s
h :
  (((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) s +
      (((κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) a) s =
    (κ a) s + (η a) s
⊢ (((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) s = (η a) s

Tactic:
rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at h

Result:
no goals

Proof state:
case hg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
⊢ Measurable (Function.uncurry fun a x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x))

Tactic:
fun_prop

Result:
no goals