-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma lintegral_toKernel_mem [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν)
    (a : α) {s : Set (β × ℝ)} (hs : MeasurableSet s) :
    ∫⁻ b, hf.toKernel f (a, b) {y | (b, y) ∈ s} ∂(ν a) = κ a s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
⊢ ∀ a ∈ t₁, {x | (a, x) ∈ t₁ ×ˢ t₂} = t₂

Tactic:
intro a ha

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
a : β
ha : a ∈ t₁
⊢ {x | (a, x) ∈ t₁ ×ˢ t₂} = t₂

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_prod_eq_snd : ∀ a ∈ t₁, {x | (a, x) ∈ t₁ ×ˢ t₂} = t₂
⊢ ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t₁ ×ˢ t₂} ∂ν a =
    ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a, x)) t₂ ∂ν a

Tactic:
refine setLIntegral_congr_fun ht₁ (Eventually.of_forall fun a ha ↦ ?_)

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_prod_eq_snd : ∀ a ∈ t₁, {x | (a, x) ∈ t₁ ×ˢ t₂} = t₂
a : β
ha : a ∈ t₁
⊢ ((IsCondKernelCDF.toKernel f hf) (a✝, a)) {y | (a, y) ∈ t₁ ×ˢ t₂} = ((IsCondKernelCDF.toKernel f hf) (a✝, a)) t₂

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ f' i} ∂ν a = (κ a) (f' i)
⊢ ∀ (a : β), {x | (a, x) ∈ ⋃ i, f' i} = ⋃ i, {x | (a, x) ∈ f' i}

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a✝, b)) {y | (b, y) ∈ f' i} ∂ν a✝ = (κ a✝) (f' i)
a : β
⊢ {x | (a, x) ∈ ⋃ i, f' i} = ⋃ i, {x | (a, x) ∈ f' i}

Proof state:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_prod_eq_snd : ∀ a ∈ t₁, {x | (a, x) ∈ t₁ ×ˢ t₂} = t₂
h_eq1 :
  ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t₁ ×ˢ t₂} ∂ν a =
    ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a, x)) t₂ ∂ν a
h_eq2 : ∫⁻ (x : β) in t₁ᶜ, ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t₁ ×ˢ t₂} ∂ν a = 0
⊢ ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a, x)) t₂ ∂ν a = (κ a) ((fun x1 x2 => x1 ×ˢ x2) t₁ t₂)

Tactic:
exact setLIntegral_toKernel_prod hf a ht₁ ht₂

Result:
no goals

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ f' i} ∂ν a = (κ a) (f' i)
h_eq : ∀ (a : β), {x | (a, x) ∈ ⋃ i, f' i} = ⋃ i, {x | (a, x) ∈ f' i}
h_disj : ∀ (a : β), Pairwise (Disjoint on fun i => {x | (a, x) ∈ f' i})
x : β
⊢ ((IsCondKernelCDF.toKernel f hf) (a, x)) (⋃ i, {y | (x, y) ∈ f' i}) =
    ∑' (i : ℕ), ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ f' i}

Tactic:
rw [measure_iUnion (h_disj x) fun i ↦ measurable_prod_mk_left (hf_meas i)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a✝, b)) {y | (b, y) ∈ f' i} ∂ν a✝ = (κ a✝) (f' i)
h_eq : ∀ (a : β), {x | (a, x) ∈ ⋃ i, f' i} = ⋃ i, {x | (a, x) ∈ f' i}
a : β
i j : ℕ
hij : i ≠ j
h_disj : (Disjoint on f') i j
⊢ (Disjoint on fun i => {x | (a, x) ∈ f' i}) i j

Tactic:
rw [Function.onFun, disjoint_iff_inter_eq_empty] at h_disj ⊢

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a✝, b)) {y | (b, y) ∈ f' i} ∂ν a✝ = (κ a✝) (f' i)
h_eq : ∀ (a : β), {x | (a, x) ∈ ⋃ i, f' i} = ⋃ i, {x | (a, x) ∈ f' i}
a : β
i j : ℕ
hij : i ≠ j
h_disj : f' i ∩ f' j = ∅
⊢ {x | (a, x) ∈ f' i} ∩ {x | (a, x) ∈ f' j} = ∅

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t} ∂ν a = (κ a) t
h_le :
  (fun x => ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t}) ≤ᶠ[ae (ν a)] fun x =>
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ ∫⁻ (a_1 : β), ((IsCondKernelCDF.toKernel f hf) (a, a_1)) univ ∂ν a < ⊤

Tactic:
rw [lintegral_toKernel_univ hf]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t} ∂ν a = (κ a) t
h_le :
  (fun x => ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t}) ≤ᶠ[ae (ν a)] fun x =>
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ
⊢ (κ a) univ < ⊤