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_1 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f_1 κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf :
  ∀ (i : ℕ),
    ∫⁻ (b : β) in s,
        (((IsCondKernelCDF.toKernel f_1 hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (f i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ f i)
⊢ ∀ (i : ℕ),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b : β) ↦
        (((IsCondKernelCDF.toKernel f_1 hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))
      (Measure.restrict ((ν : (a : α) → Measure β) a) s)

Tactic:
fun i ↦
        ((Kernel.measurable_coe _ (hf_meas i)).comp measurable_prodMk_left).aemeasurable.restrict

Premises used: Measurable.aemeasurable, Measurable.comp, AEMeasurable.restrict, ProbabilityTheory.Kernel.measurable_coe, measurable_prodMk_left, 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_1 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f_1 κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf :
  ∀ (i : ℕ),
    ∫⁻ (b : β) in s,
        (((IsCondKernelCDF.toKernel f_1 hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (f i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ f i)
⊢ ∀ (i : ℕ),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b : β) ↦
        (((IsCondKernelCDF.toKernel f_1 hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))
      (Measure.restrict ((ν : (a : α) → Measure β) a) s)

Tactic:
exact fun i ↦
        ((Kernel.measurable_coe _ (hf_meas i)).comp measurable_prodMk_left).aemeasurable.restrict

Premises used: Measurable.aemeasurable, Measurable.comp, AEMeasurable.restrict, 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 (β × ℝ)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' ∅) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) ∅

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

Premises used: MeasureTheory.lintegral_const, MulZeroClass.zero_mul, MeasureTheory.measure_empty, Set.preimage_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_1 s : Set (β × ℝ)
hs :
  Membership.mem (γ := Set (Set (β × ℝ)))
    (image2 (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) {s : Set β | MeasurableSet s} {t : Set ℝ | MeasurableSet t}) s
basic :
  ∀ (t₁ : Set β) (ht₁ : Membership.mem (γ := Set (Set β)) {s : Set β | MeasurableSet s} t₁) (t₂ : Set ℝ)
    (ht₂ : Membership.mem (γ := Set (Set ℝ)) {t : Set ℝ | MeasurableSet t} t₂),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s

Tactic:
rcases hs with ⟨t₁, ht₁, t₂, ht₂, rfl⟩

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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
basic :
  ∫⁻ (x : β) in t₁,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a +
      ∫⁻ (x : β) in t₁ᶜ,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)

Tactic:
rw [← lintegral_add_compl _ ht₁]

Premises used: MeasureTheory.lintegral_add_compl
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
⊢ ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a

Tactic:
setLIntegral_congr_fun ht₁ (fun a ha ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
refine :
  ∀ (a_1 : β) (ha : a_1 ∈ t₁),
    Eq (α := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' t₁ ×ˢ t₂) :
        ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t₂ :
        ℝ≥0∞)
⊢ ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a

Tactic:
refine setLIntegral_congr_fun ht₁ (fun a ha ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun
-- 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_1 : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
a : β
ha : a ∈ t₁
rw rw₁ :
  Eq (α := ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t₂ : ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t₂ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a ⁻¹' t₁ ×ˢ t₂) :
      ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t₂ : ℝ≥0∞)

Tactic:
rw [mk_preimage_prod_right ha]

Premises used: Set.mk_preimage_prod_right
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
⊢ ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a

Tactic:
have h_eq1 : ∫⁻ x in t₁, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν a)
        = ∫⁻ x in t₁, hf.toKernel f (a, x) t₂ ∂(ν a) := by
      refine setLIntegral_congr_fun ht₁ (fun a ha ↦ ?_)
      rw [mk_preimage_prod_right ha]
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
h_eq_zero :
  ∀ x ∈ t₁ᶜ,
    Eq (α := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t₁ ×ˢ t₂) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
rw : ∫⁻ (x : β) in t₁ᶜ, 0 ∂(ν : (a : α) → Measure β) a = 0
⊢ ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0

Tactic:
rw [setLIntegral_congr_fun ht₁.compl h_eq_zero]

Premises used: MeasureTheory.setLIntegral_congr_fun, MeasurableSet.compl
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
h_eq_zero :
  ∀ x ∈ t₁ᶜ,
    Eq (α := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t₁ ×ˢ t₂) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∫⁻ (x : β) in t₁ᶜ, 0 ∂(ν : (a : α) → Measure β) a = 0

Tactic:
simp only [lintegral_const, zero_mul]

Premises used: MeasureTheory.lintegral_const, MulZeroClass.zero_mul
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
suffices :
  ∀ x ∈ t₁ᶜ,
    Eq (α := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t₁ ×ˢ t₂) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0

Tactic:
suffices h_eq_zero :
          ∀ x ∈ t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) = 0 by
        rw [setLIntegral_congr_fun ht₁.compl h_eq_zero]
        simp only [lintegral_const, zero_mul]
-- 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_1 : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a_1 =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a_1
a : β
hat₁ : a ∈ t₁ᶜ
⊢ a ∉ t₁

Tactic:
rw [mem_compl_iff] at hat₁

Premises used: Set.mem_compl_iff
-- 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_1 : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a_1 =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a_1
a : β
hat₁ : a ∉ t₁
⊢ Eq (α := ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a ⁻¹' t₁ ×ˢ t₂) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp only [hat₁, not_false_eq_true, mk_preimage_prod_right_eq_empty, measure_empty]

Premises used: MeasureTheory.measure_empty, Set.mk_preimage_prod_right_eq_empty, not_false_eq_true
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
⊢ ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0

Tactic:
have h_eq2 :
        ∫⁻ x in t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν a) = 0 := by
      suffices h_eq_zero :
          ∀ x ∈ t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) = 0 by
        rw [setLIntegral_congr_fun ht₁.compl h_eq_zero]
        simp only [lintegral_const, zero_mul]
      intro a hat₁
      rw [mem_compl_iff] at hat₁
      simp only [hat₁, not_false_eq_true, mk_preimage_prod_right_eq_empty, measure_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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
h_eq2 :
  ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0
basic :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)
⊢ ∫⁻ (x : β) in t₁,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a +
      ∫⁻ (x : β) in t₁ᶜ,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)

Tactic:
rw [h_eq1, h_eq2, add_zero]

Premises used: add_zero
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
h_eq2 :
  ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0
⊢ ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)

Tactic:
setLIntegral_toKernel_prod hf a ht₁ ht₂

Premises used: ProbabilityTheory.setLIntegral_toKernel_prod
-- 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 (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
h_eq2 :
  ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0
⊢ ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)

Tactic:
exact setLIntegral_toKernel_prod hf a ht₁ ht₂

Premises used: ProbabilityTheory.setLIntegral_toKernel_prod
-- 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 t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' tᶜ) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t)ᶜ ∂(ν : (a : α) → Measure β) a

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Not, rfl