awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
i j : ℚ
hij : i ≤ j
⊢ SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)) ≤ SProd.sprod (β := Set ℝ) s (Iic (↑j : ℝ))

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

Premises used: Iff.mpr, Set.prod_subset_prod_iff, Set.Iic_subset_Iic, And.intro, Or.inl, subset_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
i j : ℚ
hij : i ≤ j
refine : LE.le (α := ℝ) (↑i : ℝ) (↑j : ℝ)
⊢ SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)) ≤ SProd.sprod (β := Set ℝ) s (Iic (↑j : ℝ))

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

Premises used: Iff.mpr, Set.prod_subset_prod_iff, Set.Iic_subset_Iic, And.intro, Or.inl, subset_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
i j : ℚ
hij : i ≤ j
⊢ LE.le (α := ℝ) (↑i : ℝ) (↑j : ℝ)

Tactic:
mod_cast hij

Premises used: cast, Eq.symm, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
i j : ℚ
hij : i ≤ j
⊢ LE.le (α := ℝ) (↑i : ℝ) (↑j : ℝ)

Tactic:
exact mod_cast hij
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
⊢ Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))

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
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
simp_rw :
  ∫⁻ (b : β) in s,
      ⨆ (i : ℚ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑i : ℝ)) ∂(ν : (a : α) → Measure β) a =
    ⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (r : ℚ), Iic (↑r : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))

Tactic:
simp_rw [h_dir.measure_iUnion, h_dir_prod.measure_iUnion]

Premises used: Directed.measure_iUnion
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
rw :
  Eq (α := ℝ≥0∞)
    (⨆ (b : ℚ),
      ∫⁻ (a_1 : β) in s,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)) ∂(ν : (a : α) → Measure β) a)
    (⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ))))
hf₁ :
  ∀ (b : ℚ),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b_1 : β) ↦
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)))
      (Measure.restrict ((ν : (a : α) → Measure β) a) s)
h_directed :
  Directed (fun (x1 x2 : β → ℝ≥0∞) ↦ x1 ≤ x2) fun (i : ℚ) (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑i : ℝ))
⊢ ∫⁻ (b : β) in s,
      ⨆ (i : ℚ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑i : ℝ)) ∂(ν : (a : α) → Measure β) a =
    ⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))

Tactic:
rw [lintegral_iSup_directed]

Premises used: MeasureTheory.lintegral_iSup_directed
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
⊢ Eq (α := ℝ≥0∞)
    (⨆ (b : ℚ),
      ∫⁻ (a_1 : β) in s,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)) ∂(ν : (a : α) → Measure β) a)
    (⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ))))

Tactic:
simp_rw [setLIntegral_toKernel_Iic hf _ _ hs]

Premises used: ProbabilityTheory.setLIntegral_toKernel_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
⊢ ∀ (b : ℚ),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b_1 : β) ↦
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)))
      (Measure.restrict ((ν : (a : α) → Measure β) a) s)

Tactic:
fun q ↦ Measurable.aemeasurable ?_

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
hf₁ :
  ∀ (q : ℚ),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Iic (↑q : ℝ))
⊢ ∀ (b : ℚ),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b_1 : β) ↦
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)))
      (Measure.restrict ((ν : (a : α) → Measure β) a) s)

Tactic:
refine fun q ↦ Measurable.aemeasurable ?_

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
q : ℚ
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑q : ℝ))

Tactic:
(Kernel.measurable_coe _ measurableSet_Iic).comp measurable_prodMk_left

Premises used: Measurable.comp, measurableSet_Iic, ProbabilityTheory.Kernel.measurable_coe, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
q : ℚ
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑q : ℝ))

Tactic:
exact (Kernel.measurable_coe _ measurableSet_Iic).comp measurable_prodMk_left

Premises used: Measurable.comp, measurableSet_Iic, ProbabilityTheory.Kernel.measurable_coe, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
⊢ Directed (fun (x1 x2 : β → ℝ≥0∞) ↦ x1 ≤ x2) fun (i : ℚ) (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑i : ℝ))

Tactic:
Monotone.directed_le fun i j hij t ↦ measure_mono (Iic_subset_Iic.mpr ?_)

Premises used: Iff.mpr, Set.Iic_subset_Iic, MeasureTheory.measure_mono, Monotone.directed_le
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
h_directed : ∀ (i j : ℚ) (hij : i ≤ j) (t : β), LE.le (α := ℝ) (↑i : ℝ) (↑j : ℝ)
⊢ Directed (fun (x1 x2 : β → ℝ≥0∞) ↦ x1 ≤ x2) fun (i : ℚ) (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑i : ℝ))

Tactic:
refine Monotone.directed_le fun i j hij t ↦ measure_mono (Iic_subset_Iic.mpr ?_)
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
i j : ℚ
hij : i ≤ j
t : β
⊢ LE.le (α := ℝ) (↑i : ℝ) (↑j : ℝ)

Tactic:
mod_cast hij

Premises used: cast, Eq.symm, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
i j : ℚ
hij : i ≤ j
t : β
⊢ LE.le (α := ℝ) (↑i : ℝ) (↑j : ℝ)

Tactic:
exact mod_cast hij
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
rw :
  ∫⁻ (x : β) in univ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        univ ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ
rw₁ :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) (β := Set ℝ) univ univ) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        univ ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ

Tactic:
rw [← setLIntegral_univ, setLIntegral_toKernel_univ hf a MeasurableSet.univ, univ_prod_univ]

Premises used: Set.univ_prod_univ, ProbabilityTheory.setLIntegral_toKernel_univ, MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        ∅ ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅)

Tactic:
simp only [measure_empty, lintegral_const, zero_mul, prod_empty]

Premises used: MeasureTheory.lintegral_const, MulZeroClass.zero_mul, MeasureTheory.measure_empty, Set.prod_empty
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t_1 t : Set ℝ
ht : Membership.mem (γ := Set (Set ℝ)) (range Iic) t
basic :
  ∀ (q : ℝ),
    ∫⁻ (b : β) in s,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic q) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic q)
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ t)

Tactic:
obtain ⟨q, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
q : ℝ
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Iic q) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic q)

Tactic:
setLIntegral_toKernel_Iic hf a _ hs

Premises used: ProbabilityTheory.setLIntegral_toKernel_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
q : ℝ
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Iic q) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic q)

Tactic:
exact setLIntegral_toKernel_Iic hf a _ hs

Premises used: ProbabilityTheory.setLIntegral_toKernel_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t_1 t : Set ℝ
ht : MeasurableSet t
iht :
  ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ t)
e_f :
  ∀ (x : β),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ =
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
          ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        tᶜ ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
          ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t :
          ℝ≥0∞) ∂(ν : (a : α) → Measure β) a

Tactic:
congr with x
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t_1 t : Set ℝ
ht : MeasurableSet t
iht :
  ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ t)
x : β
e_f e_f₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
        ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
        ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
        ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [measure_compl ht (measure_ne_top (hf.toKernel f (a, x)) _)]

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_ne_top, Prod.mk, DFunLike.coe, ProbabilityTheory.IsCondKernelCDF.toKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t_1 t : Set ℝ
ht : MeasurableSet t
iht :
  ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ t)
hg :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t
hg_fin :
  ∫⁻ (a_1 : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t ∂(ν : (a : α) → Measure β) a ≠
    ∞
h_le :
  (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ≥0∞)
    (fun (b : β) ↦
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t)
    fun (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ
⊢ ∫⁻ (b : β) in s,
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
          ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t :
          ℝ≥0∞) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          univ ∂(ν : (a : α) → Measure β) a -
      ∫⁻ (b : β) in s,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          t ∂(ν : (a : α) → Measure β) a

Tactic:
rw [lintegral_sub]

Premises used: MeasureTheory.lintegral_sub