awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : ℝ)))
⊢ (@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 : ℝ)))
have 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 : ℚ)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : ℚ) : ℝ)))
have 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 : ℚ))
Tactic: rw [← hf.setIntegral a hA]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : ℚ))
have refine_1 : IntegrableOn (ε := ℝ) (mα := mβ) (fun (t : β) ↦ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) A
  ((ν : (a : α) → Measure β) a)
Tactic: refine setIntegral_mono_ae ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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)
⊢ 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 : ℚ))
have refine_2 : IntegrableOn (ε := ℝ) (mα := mβ) (fun (c : β) ↦ f (a, c) (↑r : ℚ)) A ((ν : (a : α) → Measure β) a)
Tactic: refine setIntegral_mono_ae ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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)
⊢ 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 : ℚ))
have 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 : ℚ)
Tactic: refine setIntegral_mono_ae ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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)
⊢ (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ)
    (fun (t : β) ↦ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) fun (c : β) ↦ f (a, c) (↑r : ℚ)
have 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
Tactic: filter_upwards [hf.bddBelow_range a] with t ht using ciInf_le (ht _) r
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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
⊢ (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ)
    (fun (t : β) ↦ ⨅ (r' : (↑(Ioi q) : Type)), f (a, t) (↑r' : ℚ)) fun (c : β) ↦ f (a, c) (↑r : ℚ)
have h₁ : ∀ (a_1 : β),
  (∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, a_1) (↑r : ℚ))) →
    ⨅ (r' : (↑(Ioi q) : Type)), f (a, a_1) (↑r' : ℚ) ≤ f (a, a_1) (↑r : ℚ)
Tactic: filter_upwards [hf.bddBelow_range a] with t ht using ciInf_le (ht _) r
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (hypothesis)
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
⊢ (@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 : ℝ)))
have 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 : ℚ) : ℝ)))
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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : ℚ) : ℝ))) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))
have 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 : ℚ) : ℝ))))
Tactic: rw [measureReal_def, ← Measure.iInf_rat_gt_prod_Iic hA q]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : ℚ) : ℝ)))
⊢ (@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 : ℝ)))
have 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 : ℝ)))
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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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
⊢ 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 : ℚ)
have 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 : ℚ))
Tactic: rw [← hf.setIntegral a hA]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : ℚ))
have refine_2 : IntegrableOn (ε := ℝ) (mα := mβ) (fun (c : β) ↦ f (a, c) q) A ((ν : (a : α) → Measure β) a)
Tactic: refine setIntegral_mono_ae ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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)
⊢ 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 : ℚ))
have refine_2₁ : IntegrableOn (ε := ℝ) (mα := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) A
  ((ν : (a : α) → Measure β) a)
Tactic: refine setIntegral_mono_ae ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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)
⊢ 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 : ℚ))
have 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 : ℚ)
Tactic: refine setIntegral_mono_ae ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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
⊢ (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ) (fun (c : β) ↦ f (a, c) q)
    fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)
have 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
Tactic: filter_upwards [hf.mono a] with c h_mono using le_ciInf (fun r ↦ h_mono (le_of_lt r.prop))
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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
⊢ (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ) (fun (c : β) ↦ f (a, c) q)
    fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)
have h₁ : ∀ (a_1 : β), Monotone (f (a, a_1)) → f (a, a_1) q ≤ ⨅ (r : (↑(Ioi q) : Type)), f (a, a_1) (↑r : ℚ)
Tactic: filter_upwards [hf.mono a] with c h_mono using le_ciInf (fun r ↦ h_mono (le_of_lt r.prop))
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ) = f (a, t) q
have rw : ∀ (i : ℚ),
  ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ⨅ (r : (↑(Ioi i) : Type)), f (a, a_1) (↑r : ℚ) = f (a, a_1) i
Tactic: rw [ae_all_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : α
⊢ ∀ (i : ℚ),
    ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β),
      ⨅ (r : (↑(Ioi i) : Type)), f (a, a_1) (↑r : ℚ) = f (a, a_1) i
have refine_1 : ∀ (q : ℚ) (s : Set β),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, a_3) (↑r : ℚ)) s
        ((ν : (a : α) → Measure β) a)
Tactic: refine fun q ↦ ae_eq_of_forall_setIntegral_eq_of_sigmaFinite (μ := ν a) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : α
refine_1 :
  ∀ (q : ℚ) (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, a_3) (↑r : ℚ)) s
          ((ν : (a : α) → Measure β) a)
⊢ ∀ (i : ℚ),
    ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β),
      ⨅ (r : (↑(Ioi i) : Type)), f (a, a_1) (↑r : ℚ) = f (a, a_1) i
have refine_2 : ∀ (q : ℚ) (s : Set β),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ f (a, a_3) q) s ((ν : (a : α) → Measure β) a)
Tactic: refine fun q ↦ ae_eq_of_forall_setIntegral_eq_of_sigmaFinite (μ := ν a) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : α
refine_1 :
  ∀ (q : ℚ) (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, a_3) (↑r : ℚ)) s
          ((ν : (a : α) → Measure β) a)
refine_2 :
  ∀ (q : ℚ) (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ f (a, a_3) q) s ((ν : (a : α) → Measure β) a)
⊢ ∀ (i : ℚ),
    ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β),
      ⨅ (r : (↑(Ioi i) : Type)), f (a, a_1) (↑r : ℚ) = f (a, a_1) i
have refine_3 : ∀ (q : ℚ) (s : Set β),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ)
        (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
          ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ))
        (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦ f (a, x) q)
Tactic: refine fun q ↦ ae_eq_of_forall_setIntegral_eq_of_sigmaFinite (μ := ν a) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
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 : ℚ
s : Set β
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ))
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦ f (a, x) q)
have refine_3 : (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
    ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ)) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
    (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
Tactic: rw [hf.setIntegral _ hs, hf.setIntegral_iInf_rat_gt _ _ hs]