-- Mathlib/Probability/Kernel/RadonNikodym.lean
@[fun_prop]
lemma measurable_rnDerivAux (κ η : Kernel α γ) :
    Measurable (fun p : α × γ ↦ Kernel.rnDerivAux κ η p.1 p.2)

Proof state:
case pos.refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
h_eq : ∀ (κ : Kernel α γ), κ a' = κ a
⊢ (∂κ (c, a').2/∂η (c, a').2) (c, a').1 = (∂κ (c, a).2/∂η (c, a).2) (c, a).1

Tactic:
rw [h_eq κ, h_eq η]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p => κ.rnDerivAux η p.1 p.2

Tactic:
simp_rw [rnDerivAux]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p =>
    if hα : Countable α then ((∂κ p.1/∂η p.1) p.2).toReal else (κ.map fun a => (a, ())).density η p.1 p.2 univ

Proof state:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Measurable fun p => (κ.map fun a => (a, ())).density η p.1 p.2 univ

Tactic:
exact measurable_density _ η MeasurableSet.univ

Result:
no goals

Proof state:
case pos.refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
a : α
⊢ Measurable fun x => (∂κ (x, a).2/∂η (x, a).2) (x, a).1

Tactic:
exact Measure.measurable_rnDeriv (κ a) (η a)

Result:
no goals

Proof state:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
⊢ Measurable fun p => (κ.map fun a => (a, ())).density η p.1 p.2 univ

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

Result:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Measurable fun p => (κ.map fun a => (a, ())).density η p.1 p.2 univ

Proof state:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable ((fun q => (∂κ q.2/∂η q.2) q.1) ∘ Prod.swap)

Tactic:
refine (measurable_from_prod_countable' (fun a ↦ ?_) ?_).comp measurable_swap

Result:
case pos.refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
a : α
⊢ Measurable fun x => (∂κ (x, a).2/∂η (x, a).2) (x, a).1

case pos.refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ ∀ (y y' : α) (x : γ),
    y' ∈ measurableAtom y → (∂κ (x, y').2/∂η (x, y').2) (x, y').1 = (∂κ (x, y).2/∂η (x, y).2) (x, y).1

Proof state:
case pos.refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
⊢ (∂κ (c, a').2/∂η (c, a').2) (c, a').1 = (∂κ (c, a).2/∂η (c, a).2) (c, a).1

Tactic:
have h_eq : ∀ κ : Kernel α γ, κ a' = κ a := fun κ ↦ by
  ext s hs
  exact mem_of_mem_measurableAtom ha'_mem_a
    (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl

Result:
case pos.refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
h_eq : ∀ (κ : Kernel α γ), κ a' = κ a
⊢ (∂κ (c, a').2/∂η (c, a').2) (c, a').1 = (∂κ (c, a).2/∂η (c, a).2) (c, a).1

Proof state:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable fun p => ((∂κ p.1/∂η p.1) p.2).toReal

Tactic:
refine Measurable.ennreal_toReal ?_

Result:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable fun p => (∂κ p.1/∂η p.1) p.2

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ✝ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
κ : Kernel α γ
⊢ κ a' = κ a

Tactic:
ext s hs

Result:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ✝ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
⊢ (κ a') s = (κ a) s

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p =>
    if hα : Countable α then ((∂κ p.1/∂η p.1) p.2).toReal else (κ.map fun a => (a, ())).density η p.1 p.2 univ

Tactic:
split_ifs with hα

Result:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable fun p => ((∂κ p.1/∂η p.1) p.2).toReal

case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
⊢ Measurable fun p => (κ.map fun a => (a, ())).density η p.1 p.2 univ

Proof state:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ✝ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
⊢ (κ a') s = (κ a) s

Tactic:
exact mem_of_mem_measurableAtom ha'_mem_a
  (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable fun p => (∂κ p.1/∂η p.1) p.2

Tactic:
change Measurable ((fun q : γ × α ↦ (κ q.2).rnDeriv (η q.2) q.1) ∘ Prod.swap)

Result:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable ((fun q => (∂κ q.2/∂η q.2) q.1) ∘ Prod.swap)

Proof state:
case pos.refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ ∀ (y y' : α) (x : γ),
    y' ∈ measurableAtom y → (∂κ (x, y').2/∂η (x, y').2) (x, y').1 = (∂κ (x, y).2/∂η (x, y).2) (x, y).1

Tactic:
intro a a' c ha'_mem_a

Result:
case pos.refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
⊢ (∂κ (c, a').2/∂η (c, a').2) (c, a').1 = (∂κ (c, a).2/∂η (c, a).2) (c, a).1