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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
refine_1 :
  (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ≤
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))
refine_2 :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ))) ≤
    @integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
rw :
  LE.le (α := ℝ)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ))
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (c : β) ↦ f (a, c) (↑r : ℚ))
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) ≤
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ)))

Tactic:
rw [← hf.setIntegral a hA]

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ))
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (c : β) ↦ f (a, c) (↑r : ℚ))

Tactic:
setIntegral_mono_ae ?_ ?_ ?_

Premises used: MeasureTheory.setIntegral_mono_ae
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
refine_1 :
  IntegrableOn (ε := ℝ) (mα := mβ) (fun (t : β) ↦ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) A
    ((ν : (a : α) → Measure β) a)
refine_2 : IntegrableOn (ε := ℝ) (mα := mβ) (fun (c : β) ↦ f (a, c) (↑r : ℚ)) A ((ν : (a : α) → Measure β) a)
refine_3 :
  (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ)
    (fun (t : β) ↦ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) fun (c : β) ↦ f (a, c) (↑r : ℚ)
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ))
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (c : β) ↦ f (a, c) (↑r : ℚ))

Tactic:
refine setIntegral_mono_ae ?_ ?_ ?_

Premises used: MeasureTheory.setIntegral_mono_ae
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
⊢ IntegrableOn (ε := ℝ) (mα := mβ) (fun (t : β) ↦ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) A
    ((ν : (a : α) → Measure β) a)

Tactic:
(hf.integrable_iInf_rat_gt _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, MeasureTheory.Integrable.integrableOn
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
⊢ IntegrableOn (ε := ℝ) (mα := mβ) (fun (t : β) ↦ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) A
    ((ν : (a : α) → Measure β) a)

Tactic:
exact (hf.integrable_iInf_rat_gt _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, MeasureTheory.Integrable.integrableOn
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
⊢ IntegrableOn (ε := ℝ) (mα := mβ) (fun (c : β) ↦ f (a, c) (↑r : ℚ)) A ((ν : (a : α) → Measure β) a)

Tactic:
(hf.integrable _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable, MeasureTheory.Integrable.integrableOn
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
⊢ IntegrableOn (ε := ℝ) (mα := mβ) (fun (c : β) ↦ f (a, c) (↑r : ℚ)) A ((ν : (a : α) → Measure β) a)

Tactic:
exact (hf.integrable _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable, MeasureTheory.Integrable.integrableOn
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
t : β
ht : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
⊢ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ) ≤ f (a, t) (↑r : ℚ)

Tactic:
ciInf_le (ht _) r

Premises used: ciInf_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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
r : (↑(Ioi q) : Type)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (t : β) ↦ ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))) x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  LE.le (α := ℝ) ((fun (t : β) ↦ (⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ) : ℝ)) x)
                    ((fun (c : β) ↦ f (a, c) (↑r : ℚ)) x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (t : β) (ht : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))),
    ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ) ≤ f (a, t) (↑r : ℚ)
⊢ (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ)
    (fun (t : β) ↦ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) fun (c : β) ↦ f (a, c) (↑r : ℚ)

Tactic:
filter_upwards [hf.bddBelow_range a] with t ht using ciInf_le (ht _) r

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.bddBelow_range
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∀ (r : (↑(Ioi q) : Type)),
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
        ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) ≤
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ)))

Tactic:
have h : ∀ r : Ioi q, ∫ t in A, ⨅ r' : Ioi q, f (a, t) r' ∂(ν a)
        ≤ (κ a).real (A ×ˢ Iic (r : ℝ)) := by
      intro r
      rw [← hf.setIntegral a hA]
      refine setIntegral_mono_ae ?_ ?_ ?_
      · exact (hf.integrable_iInf_rat_gt _ _).integrableOn
      · exact (hf.integrable _ _).integrableOn
      · filter_upwards [hf.bddBelow_range a] with t ht using ciInf_le (ht _) r
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h :
  ∀ (r : (↑(Ioi q) : Type)),
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
        ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) ≤
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ)))
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ))
    (⨅ (r : (↑(Ioi q) : Type)),
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))))

Tactic:
le_ciInf h

Premises used: le_ciInf
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h :
  ∀ (r : (↑(Ioi q) : Type)),
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
        ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) ≤
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ)))
rw :
  ⨅ (r : (↑(Ioi q) : Type)),
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))) =
    ENNReal.toReal
      (⨅ (r : { r' : ℚ // q < r' }),
        (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
          (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))))
⊢ ⨅ (r : (↑(Ioi q) : Type)),
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))

Tactic:
rw [measureReal_def, ← Measure.iInf_rat_gt_prod_Iic hA q]

Premises used: MeasureTheory.Measure.iInf_rat_gt_prod_Iic, MeasureTheory.measureReal_def
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h :
  ∀ (r : (↑(Ioi q) : Type)),
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
        ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) ≤
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ)))
⊢ ⨅ (r : (↑(Ioi q) : Type)),
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))) =
    ENNReal.toReal
      (⨅ (r : { r' : ℚ // q < r' }),
        (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
          (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))))

Tactic:
(ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

Premises used: Set.Ioi, Set.Mem, setOf, MeasureTheory.Measure.real, MeasureTheory.measure_ne_top, ENNReal.toReal_iInf, Eq.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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h :
  ∀ (r : (↑(Ioi q) : Type)),
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
        ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) ≤
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ)))
⊢ ⨅ (r : (↑(Ioi q) : Type)),
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))) =
    ENNReal.toReal
      (⨅ (r : { r' : ℚ // q < r' }),
        (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
          (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))))

Tactic:
exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

Premises used: MeasureTheory.measure_ne_top, ENNReal.toReal_iInf, Eq.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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h :
  ∀ (r : (↑(Ioi q) : Type)),
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
        ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) ≤
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ)))
calc :
  ⨅ (r : (↑(Ioi q) : Type)),
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) A (Iic (↑(↑r : ℚ) : ℝ))) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ≤
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))

Tactic:
calc ∫ t in A, ⨅ r : Ioi q, f (a, t) r ∂(ν a)
      ≤ ⨅ r : Ioi q, (κ a).real (A ×ˢ Iic (r : ℝ)) := le_ciInf h
    _ = (κ a).real (A ×ˢ Iic (q : ℝ)) := by
        rw [measureReal_def, ← Measure.iInf_rat_gt_prod_Iic hA q]
        exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

Premises used: Set.Ioi, SProd.sprod, MeasureTheory.Measure.real, Rat.cast, le_ciInf, Set.Iic, 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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
refine_2 :
  LE.le (α := ℝ) (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (c : β) ↦ f (a, c) q)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ))
⊢ Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ))) ≤
    @integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)

Tactic:
rw [← hf.setIntegral a hA]

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ LE.le (α := ℝ) (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (c : β) ↦ f (a, c) q)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ))

Tactic:
setIntegral_mono_ae ?_ ?_ ?_

Premises used: MeasureTheory.setIntegral_mono_ae
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
refine_2 : IntegrableOn (ε := ℝ) (mα := mβ) (fun (c : β) ↦ f (a, c) q) A ((ν : (a : α) → Measure β) a)
refine_2₁ :
  IntegrableOn (ε := ℝ) (mα := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) A
    ((ν : (a : α) → Measure β) a)
refine_2₂ :
  (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ) (fun (c : β) ↦ f (a, c) q)
    fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)
⊢ LE.le (α := ℝ) (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (c : β) ↦ f (a, c) q)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ))

Tactic:
refine setIntegral_mono_ae ?_ ?_ ?_

Premises used: MeasureTheory.setIntegral_mono_ae
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ IntegrableOn (ε := ℝ) (mα := mβ) (fun (c : β) ↦ f (a, c) q) A ((ν : (a : α) → Measure β) a)

Tactic:
(hf.integrable _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable, MeasureTheory.Integrable.integrableOn
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ IntegrableOn (ε := ℝ) (mα := mβ) (fun (c : β) ↦ f (a, c) q) A ((ν : (a : α) → Measure β) a)

Tactic:
exact (hf.integrable _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable, MeasureTheory.Integrable.integrableOn
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ IntegrableOn (ε := ℝ) (mα := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) A
    ((ν : (a : α) → Measure β) a)

Tactic:
(hf.integrable_iInf_rat_gt _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, MeasureTheory.Integrable.integrableOn
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ IntegrableOn (ε := ℝ) (mα := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) A
    ((ν : (a : α) → Measure β) a)

Tactic:
exact (hf.integrable_iInf_rat_gt _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, MeasureTheory.Integrable.integrableOn
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
c : β
h_mono : Monotone (f (a, c))
⊢ f (a, c) q ≤ ⨅ (r : (↑(Ioi q) : Type)), f (a, c) (↑r : ℚ)

Tactic:
le_ciInf (fun r ↦ h_mono (le_of_lt r.prop))

Premises used: le_of_lt, le_ciInf, Subtype.prop
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ Monotone (f (a, c))) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  LE.le (α := ℝ) ((fun (c : β) ↦ f (a, c) q) x)
                    ((fun (t : β) ↦ (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ) : ℝ)) x))
                x}
            x}
      a_1
h₁ h₂ : ∀ (c : β) (h_mono : Monotone (f (a, c))), f (a, c) q ≤ ⨅ (r : (↑(Ioi q) : Type)), f (a, c) (↑r : ℚ)
⊢ (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ) (fun (c : β) ↦ f (a, c) q)
    fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)

Tactic:
filter_upwards [hf.mono a] with c h_mono using le_ciInf (fun r ↦ h_mono (le_of_lt r.prop))

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.mono
-- 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
rw :
  ∀ (i : ℚ),
    ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β),
      ⨅ (r : (↑(Ioi i) : Type)), f (a, a_1) (↑r : ℚ) = f (a, a_1) i
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ) = f (a, t) q

Tactic:
rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff