-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma setLIntegral_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η]
    (a : α) {s : Set γ} (hs : MeasurableSet s) :
    ∫⁻ x in s, ENNReal.ofReal (rnDerivAux κ (κ + η) a x) ∂(κ + η) a = κ a s

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Measurable fun a => (a, ())

Tactic:
fun_prop

Result:
no goals

Proof state:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac : κ a ≪ (κ + η) a
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal ∂(κ + η) a = (κ a) s

Tactic:
rw [← Measure.setLIntegral_rnDeriv h_ac]

Result:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac : κ a ≪ (κ + η) a
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal ∂(κ + η) a =
    ∫⁻ (x : γ) in s, (∂κ a/∂(κ + η) a) x ∂(κ + η) a

Proof state:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((κ.map fun a => (a, ())).density (κ + η) a x univ) ∂(κ + η) a = (κ a) s

Tactic:
have := hαγ.countableOrCountablyGenerated.resolve_left hα

Result:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((κ.map fun a => (a, ())).density (κ + η) a x univ) ∂(κ + η) a = (κ a) s

Proof state:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac : κ a ≪ (κ + η) a
⊢ ∀ᵐ (x : γ) ∂(κ + η) a, x ∈ s → ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal = (∂κ a/∂(κ + η) a) x

Tactic:
filter_upwards [Measure.rnDeriv_lt_top (κ a) ((κ + η) a)] with x hx_lt _

Result:
case 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
h_le : κ ≤ κ + η
hα : Countable α
h_ac : κ a ≪ (κ + η) a
x : γ
hx_lt : (∂κ a/∂(κ + η) a) x < ⊤
a✝ : x ∈ s
⊢ ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal = (∂κ a/∂(κ + η) a) x

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
⊢ ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (if hα : Countable α then ((∂κ a/∂(κ + η) a) x).toReal
        else (κ.map fun a => (a, ())).density (κ + η) a x univ) ∂(κ + η) a =
    (κ a) s

Tactic:
split_ifs with hα

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

case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((κ.map fun a => (a, ())).density (κ + η) a x univ) ∂(κ + η) a = (κ a) s

Proof state:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ (κ a) ((fun a => (a, ())) ⁻¹' s ×ˢ univ) = (κ a) s

Tactic:
congr with x

Result:
case neg.h.e_6.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
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
x : γ
⊢ x ∈ (fun a => (a, ())) ⁻¹' s ×ˢ univ ↔ x ∈ s

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

Tactic:
have h_ac : κ a ≪ (κ + η) a := Measure.absolutelyContinuous_of_le (h_le a)

Result:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac : κ a ≪ (κ + η) a
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal ∂(κ + η) a = (κ a) s

Proof state:
case 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
h_le : κ ≤ κ + η
hα : Countable α
h_ac : κ a ≪ (κ + η) a
x : γ
hx_lt : (∂κ a/∂(κ + η) a) x < ⊤
a✝ : x ∈ s
⊢ ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal = (∂κ a/∂(κ + η) a) x

Tactic:
rw [ENNReal.ofReal_toReal hx_lt.ne]

Result:
no goals

Proof state:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((κ.map fun a => (a, ())).density (κ + η) a x univ) ∂(κ + η) a = (κ a) s

Tactic:
rw [setLIntegral_density ((fst_map_id_prod _ measurable_const).trans_le h_le) _
  MeasurableSet.univ hs, map_apply' _ (by fun_prop) _ (hs.prod MeasurableSet.univ)]

Result:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ (κ a) ((fun a => (a, ())) ⁻¹' s ×ˢ univ) = (κ a) s