-- 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 t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t} ∂ν a = (κ a) t
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t}ᶜ ∂ν a =
    ∫⁻ (b : β),
      ((IsCondKernelCDF.toKernel f hf) (a, b)) univ - ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t} ∂ν a

Tactic:
congr with x : 1

Result:
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 t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t} ∂ν a = (κ a) t
x : β
⊢ ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ t}ᶜ =
    ((IsCondKernelCDF.toKernel f hf) (a, x)) univ - ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ 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)
h_eq : ∀ (a : β), {x | (a, x) ∈ ⋃ i, f' i} = ⋃ i, {x | (a, x) ∈ f' i}
⊢ ∀ (a : β), Pairwise (Disjoint on fun i => {x | (a, x) ∈ f' i})

Tactic:
intro a i j hij

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
⊢ (Disjoint on fun i => {x | (a, x) ∈ f' i}) i j

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

Tactic:
rw [mem_compl_iff] at hat₁

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✝
a : β
hat₁ : a ∉ t₁
⊢ ((IsCondKernelCDF.toKernel f hf) (a✝, a)) {y | (a, y) ∈ t₁ ×ˢ t₂} = 0

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✝
a : β
hat₁ : a ∉ t₁
⊢ ((IsCondKernelCDF.toKernel f hf) (a✝, a)) {y | (a, y) ∈ t₁ ×ˢ t₂} = 0

Tactic:
simp only [hat₁, prod_mk_mem_set_prod_eq, false_and, setOf_false, measure_empty]

Result:
no goals

Proof state:
case 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}
a : β
i j : ℕ
hij : i ≠ j
h_disj : f' i ∩ f' j = ∅
x : ℝ
⊢ x ∈ {x | (a, x) ∈ f' i} ∩ {x | (a, x) ∈ f' j} ↔ x ∈ ∅

Tactic:
simp only [mem_inter_iff, mem_setOf_eq, mem_empty_iff_false, iff_false]

Result:
case 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}
a : β
i j : ℕ
hij : i ≠ j
h_disj : f' i ∩ f' j = ∅
x : ℝ
⊢ ¬((a, x) ∈ f' i ∧ (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) univ < ⊤

Tactic:
exact measure_lt_top _ univ

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}
h_disj : ∀ (a : β), Pairwise (Disjoint on fun i => {x | (a, x) ∈ f' i})
⊢ ∑' (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ f' i} ∂ν a = ∑' (i : ℕ), (κ a) (f' i)

Tactic:
simp_rw [hf_eq]

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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
a : β
ha : a ∈ t₁
⊢ {x | (a, x) ∈ t₁ ×ˢ t₂} = t₂

Tactic:
simp only [ha, prod_mk_mem_set_prod_eq, true_and, setOf_mem_eq]

Result:
no goals