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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ) ((fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) x)
                    ((fun (b : β) ↦ f (a, b) q) x))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  x ∈ s → (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ) = (fun (b : β) ↦ f (a, b) q) x)
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (b : β) (hb : (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ) = f (a, b) q),
    b ∈ s → (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ) = f (a, b) q
⊢ ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    x ∈ s → (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ) = (fun (b : β) ↦ f (a, b) q) x

Tactic:
filter_upwards [stieltjesOfMeasurableRat_ae_eq hf a q] with b hb using fun _ ↦ hb

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ)) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
hfi :
  @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ))
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)
f_nn :
  (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ) 0 fun (b : β) ↦
    (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)
⊢ ∫⁻ (b : β) in s,
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal]

Premises used: MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
rw :
  ENNReal.ofReal
      (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₁ rw₂ :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
⊢ ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ)) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))

Tactic:
rw [setIntegral_stieltjesOfMeasurableRat_rat hf a q hs, ofReal_measureReal]

Premises used: MeasureTheory.ofReal_measureReal, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ))
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)

Tactic:
Integrable.restrict ?_

Premises used: MeasureTheory.Integrable.restrict
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
hfi :
  @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ))
    ((ν : (a : α) → Measure β) a)
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ))
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)

Tactic:
refine Integrable.restrict ?_

Premises used: MeasureTheory.Integrable.restrict
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
hfi : @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ f (a, b) q) ((ν : (a : α) → Measure β) a)
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ))
    ((ν : (a : α) → Measure β) a)

Tactic:
rw [integrable_congr (stieltjesOfMeasurableRat_ae_eq hf a q)]

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq, MeasureTheory.integrable_congr
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ f (a, b) q) ((ν : (a : α) → Measure β) a)

Tactic:
hf.integrable a q

Premises used: ProbabilityTheory.IsRatCondKernelCDF.integrable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ f (a, b) q) ((ν : (a : α) → Measure β) a)

Tactic:
exact hf.integrable a q

Premises used: ProbabilityTheory.IsRatCondKernelCDF.integrable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ) 0 fun (b : β) ↦
    (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)

Tactic:
ae_of_all _ (fun x ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_nonneg, Rat.cast, Prod.mk, MeasureTheory.ae_of_all, ProbabilityTheory.IsRatCondKernelCDF.measurable, Filter.EventuallyLE
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ) 0 fun (b : β) ↦
    (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)

Tactic:
exact ae_of_all _ (fun x ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_nonneg, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
pos :
  ∀ (hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0),
    ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
neg :
  ∀ (hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0),
    ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)

Tactic:
by_cases hρ_zero : (ν a).restrict s = 0

Premises used: MeasureTheory.Measure.restrict, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
pos :
  Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)

Tactic:
rw [hρ_zero, lintegral_zero_measure]

Premises used: MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
pos :
  ∀ (q : ℚ) (hq : x < (↑q : ℝ)),
    Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)

Tactic:
have ⟨q, hq⟩ := exists_rat_gt 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
symm :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)

Tactic:
symm
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null (fun p ↦ ?_) this

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
refine : ∀ p ∈ s ×ˢ Iic x, p ∈ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null (fun p ↦ ?_) this

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
p : β × ℝ
simp : p.1 ∈ s → p.2 ≤ x → p.1 ∈ s ∧ p.2 ≤ (↑q : ℝ)
⊢ p ∈ s ×ˢ Iic x → p ∈ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))

Tactic:
simp only [mem_prod, mem_Iic, and_imp]

Premises used: and_imp, Set.mem_prod, Set.mem_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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
p : β × ℝ
⊢ p.1 ∈ s → p.2 ≤ x → p.1 ∈ s ∧ p.2 ≤ (↑q : ℝ)

Tactic:
fun h1 h2 ↦ ⟨h1, h2.trans hq.le⟩

Premises used: LT.lt.le, And.intro, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
p : β × ℝ
⊢ p.1 ∈ s → p.2 ≤ x → p.1 ∈ s ∧ p.2 ≤ (↑q : ℝ)

Tactic:
exact fun h1 h2 ↦ ⟨h1, h2.trans hq.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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
pos :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)

Tactic:
suffices κ a (s ×ˢ Iic (q : ℝ)) = 0 by
      symm
      refine measure_mono_null (fun p ↦ ?_) this
      simp only [mem_prod, mem_Iic, and_imp]
      exact fun h1 h2 ↦ ⟨h1, h2.trans hq.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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
this :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) =
    0
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [measureReal_eq_zero_iff] at this

Premises used: MeasureTheory.measureReal_eq_zero_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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simpa [measure_ne_top] using this

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
pos :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) =
    0
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
suffices (κ a).real (s ×ˢ Iic (q : ℝ)) = 0 by
      rw [measureReal_eq_zero_iff] at this
      simpa [measure_ne_top] using this
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
pos : Eq (α := ℝ) (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦ f (a, b) q) 0
⊢ Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) =
    0

Tactic:
rw [← hf.setIntegral a hs q]

Premises used: ProbabilityTheory.IsRatCondKernelCDF.setIntegral
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
⊢ Eq (α := ℝ) (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦ f (a, b) q) 0

Tactic:
simp [hρ_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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
e_f :
  ∀ (b : β),
    ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a

Tactic:
congr with b : 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
e_f :
  Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑r : ℚ) : ℝ)) :
      ℝ≥0∞)
⊢ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))

Tactic:
simp_rw [← measure_stieltjesOfMeasurableRat_Iic]

Premises used: ProbabilityTheory.measure_stieltjesOfMeasurableRat_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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
e_f :
  Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) :
      ℝ≥0∞)
e_f₁ : Monotone (β := Set ℝ) fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ Iic (↑(↑r : ℚ) : ℝ)
e_f₂ :
  ∀ (i : { r' : ℚ // x < (↑r' : ℝ) }),
    NullMeasurableSet (Iic (↑(↑i : ℚ) : ℝ)) (stieltjesOfMeasurableRat f ⋯ (a, b)).measure
e_f₃ :
  ∃ (i : { r' : ℚ // x < (↑r' : ℝ) }),
    Ne (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑i : ℚ) : ℝ)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑r : ℚ) : ℝ)) :
      ℝ≥0∞)

Tactic:
rw [← Monotone.measure_iInter]

Premises used: Monotone.measure_iInter