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

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑i)

Tactic:
have h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ s ×ˢ Iic (q : ℝ) := by
  refine Monotone.directed_le fun i j hij ↦ ?_
  refine prod_subset_prod_iff.mpr (Or.inl ⟨subset_rfl, Iic_subset_Iic.mpr ?_⟩)
  exact mod_cast hij

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q
h_dir_prod : Directed (fun x y => x ⊆ y) fun q => s ×ˢ Iic ↑q
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑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 β
hs : MeasurableSet s
⊢ Directed (fun x y => x ⊆ y) fun q => Iic ↑q

Tactic:
refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
r r' : ℚ
hrr' : r ≤ r'
⊢ ↑r ≤ ↑r'

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑i)

Tactic:
have h_dir : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ Iic (q : ℝ) := by
  refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_
  exact mod_cast hrr'

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑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 β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a = (κ a) (s ×ˢ univ)

Tactic:
rw [← Real.iUnion_Iic_rat, prod_iUnion]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑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 β
hs : MeasurableSet s
h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q
i j : ℚ
hij : i ≤ j
⊢ s ×ˢ Iic ↑i ≤ s ×ˢ Iic ↑j

Tactic:
refine prod_subset_prod_iff.mpr (Or.inl ⟨subset_rfl, Iic_subset_Iic.mpr ?_⟩)

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q
i j : ℚ
hij : i ≤ j
⊢ ↑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 β
hs : MeasurableSet s
h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q
⊢ Directed (fun x y => x ⊆ y) fun q => s ×ˢ Iic ↑q

Tactic:
refine Monotone.directed_le fun 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 β
hs : MeasurableSet s
h_dir : Directed (fun x y => x ⊆ y) fun q => Iic ↑q
i j : ℚ
hij : i ≤ j
⊢ s ×ˢ Iic ↑i ≤ s ×ˢ Iic ↑j