-- 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₂
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
⊢ ∫⁻ (x : β) in t₁ᶜ, ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t₁ ×ˢ t₂} ∂ν a = 0

Tactic:
suffices h_eq_zero :
    ∀ x ∈ t₁ᶜ, hf.toKernel f (a, x) {y : ℝ | (x, y) ∈ t₁ ×ˢ t₂} = 0 by
  rw [setLIntegral_congr_fun ht₁.compl (Eventually.of_forall h_eq_zero)]
  simp only [lintegral_const, zero_mul]

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₂
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
⊢ ∀ x ∈ t₁ᶜ, ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t₁ ×ˢ t₂} = 0

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₂
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ (fun x1 x2 => x1 ×ˢ x2) t₁ t₂} ∂ν a =
    (κ a) ((fun x1 x2 => x1 ×ˢ x2) t₁ t₂)

Tactic:
have h_prod_eq_snd : ∀ a ∈ t₁, {x : ℝ | (a, x) ∈ t₁ ×ˢ t₂} = t₂ := by
  intro a ha
  simp only [ha, prod_mk_mem_set_prod_eq, true_and, setOf_mem_eq]

Result:
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₂
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ (fun x1 x2 => x1 ×ˢ x2) t₁ t₂} ∂ν a =
    (κ a) ((fun x1 x2 => x1 ×ˢ x2) 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 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)) {y | (a_1, y) ∈ t} ∂ν a ≠ ⊤

Tactic:
refine ((lintegral_mono_ae h_le).trans_lt ?_).ne

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_1 : β), ((IsCondKernelCDF.toKernel f hf) (a, a_1)) univ ∂ν a < ⊤

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
⊢ ∫⁻ (b : β),
      ((IsCondKernelCDF.toKernel f hf) (a, b)) univ - ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t} ∂ν a =
    ∫⁻ (x : β), ((IsCondKernelCDF.toKernel f hf) (a, x)) univ ∂ν a -
      ∫⁻ (x : β), ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t} ∂ν a

Tactic:
rw [lintegral_sub _ _ h_le]

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
⊢ Measurable fun x => ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t}

α : 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)) {y | (a_1, y) ∈ t} ∂ν a ≠ ⊤

Proof state:
case iUnion
α : 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}
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ i, {x | (b, x) ∈ f' i}) ∂ν a = (κ a) (⋃ i, f' i)

Tactic:
have h_disj : ∀ a, Pairwise (Disjoint on fun i ↦ {x | (a, x) ∈ f' i}) := by
  intro a i j hij
  have h_disj := hf_disj hij
  rw [Function.onFun, disjoint_iff_inter_eq_empty] at h_disj ⊢
  ext1 x
  simp only [mem_inter_iff, mem_setOf_eq, mem_empty_iff_false, iff_false]
  intro h_mem_both
  suffices (a, x) ∈ ∅ by rwa [mem_empty_iff_false] at this
  rwa [← h_disj, mem_inter_iff]

Result:
case iUnion
α : 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})
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ i, {x | (b, x) ∈ f' i}) ∂ν a = (κ a) (⋃ i, f' i)