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

Tactic:
have h_eq2 :
    ∫⁻ x in t₁ᶜ, hf.toKernel f (a, x) {y : ℝ | (x, y) ∈ t₁ ×ˢ t₂} ∂(ν a) = 0 := by
  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]
  intro a hat₁
  rw [mem_compl_iff] at hat₁
  simp only [hat₁, prod_mk_mem_set_prod_eq, false_and, setOf_false, measure_empty]

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

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

Tactic:
have h_eq1 : ∫⁻ x in t₁, hf.toKernel f (a, x) {y : ℝ | (x, y) ∈ t₁ ×ˢ t₂} ∂(ν a)
    = ∫⁻ x in t₁, hf.toKernel f (a, x) t₂ ∂(ν a) := by
  refine setLIntegral_congr_fun ht₁ (Eventually.of_forall fun a ha ↦ ?_)
  rw [h_prod_eq_snd a ha]

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

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

Tactic:
have h_eq : ∀ a, {x | (a, x) ∈ ⋃ i, f' i} = ⋃ i, {x | (a, x) ∈ f' i} := by
  intro a; ext x; simp only [mem_iUnion, mem_setOf_eq]

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

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})
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ i, {y | (b, y) ∈ f' i}) ∂ν a =
    ∫⁻ (b : β), ∑' (i : ℕ), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ f' i} ∂ν 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 : 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}