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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)
have rw : ENNReal.ofReal
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x) =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
Tactic: rw [← ENNReal.ofReal_eq_ofReal_iff, ofReal_measureReal]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)
have hp : LE.le (α := ℝ) 0
  (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
    (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x)
Tactic: rw [← ENNReal.ofReal_eq_ofReal_iff, ofReal_measureReal]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
hp :
  LE.le (α := ℝ) 0
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)
have hq : 0 ≤ Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)
Tactic: rw [← ENNReal.ofReal_eq_ofReal_iff, ofReal_measureReal]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have hfi : @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x)
  (Measure.restrict ((ν : (a : α) → Measure β) a) s)
Tactic: rw [ofReal_integral_eq_lintegral_ofReal, setLIntegral_stieltjesOfMeasurableRat hf _ _ hs]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hfi :
  @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)
⊢ ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have f_nn : (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ) 0 fun (b : β) ↦
  (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x
Tactic: rw [ofReal_integral_eq_lintegral_ofReal, setLIntegral_stieltjesOfMeasurableRat hf _ _ hs]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))
have rw : (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) univ) fun (x_1 : β) ↦
    (↑(stieltjesOfMeasurableRat f sorry (a, x_1)) : ℝ → ℝ) x) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
    (SProd.sprod (α := Set β) univ (Iic x))
Tactic: rw [← setIntegral_univ, setIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
rw :
  (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) univ) fun (x_1 : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))
⊢ (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))
have rw₁ : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
    (SProd.sprod (α := Set β) univ (Iic x)) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
    (SProd.sprod (α := Set β) univ (Iic x))
Tactic: rw [← setIntegral_univ, setIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]
-- 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 κ ν
a : α
q : ℚ
h : Measurable f := ⋯
⊢ Measurable (β := ℝ) fun (t : β) ↦ f (a, t) q
have h₁ : ∀ (a : ℚ), Measurable (β := ℝ) fun (x : α × β) ↦ f x a
Tactic: rw [measurable_pi_iff] at h
Cleared hypotheses: h
-- 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 κ ν
a : α
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ ⦃a_1 b : ℚ⦄, a_1 ≤ b → f (a, c) a_1 ≤ f (a, c) b
have simp_rw : ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), f (a, a_1) i ≤ f (a, a_1) i_1
Tactic: simp_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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 0)
have refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
Tactic: refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 0)
have refine_2 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
  atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 0))
Tactic: refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
refine_2 :
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 0))
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 0)
have refine_3 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
Tactic: refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
refine_2 :
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 0))
refine_3 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 0)
have refine_4 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)
Tactic: refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 0))
have refine_2 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
  atTop (𝓝 0)
Tactic: rw [integral_zero]
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
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 (a_3 : β) ↦ Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_3) (seq i)) x} x}
    a_1
Tactic: filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ Monotone (f (a, c))) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_3) (seq i)) x}
            x}
      a_1
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
have h₁ : ∀ (a_1 : β), Monotone (f (a, a_1)) → Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
Tactic: filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ ∀ (q : ℚ), 0 ≤ f (a, c) q) x} x →
        Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ ∀ (i : ℕ), 0 ≤ f (a, a_3) (seq i)) x} x}
    a_1
Tactic: filter_upwards [hf.nonneg a] with c hc using fun i ↦ hc (seq i)
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ ∀ (q : ℚ), 0 ≤ f (a, c) q) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ ∀ (i : ℕ), 0 ≤ f (a, a_3) (seq i)) x} x}
      a_1
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)
have h₁ : ∀ (a_1 : β), (∀ (q : ℚ), 0 ≤ f (a, a_1) q) → ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)
Tactic: filter_upwards [hf.nonneg a] with c hc using fun i ↦ hc (seq i)
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 1)
have refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
Tactic: refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 1)
have refine_2 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
  atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 1))
Tactic: refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
refine_2 :
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 1))
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 1)
have refine_3 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
Tactic: refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
refine_2 :
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 1))
refine_3 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 1)
have refine_4 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), f (a, a_1) (seq i) ≤ 1
Tactic: refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 1))
have refine_2 : Tendsto (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i)) atTop
  (𝓝 (Measure.real.{u_2} (α := β) (m := mβ) ((ν : (a : α) → Measure β) a) univ))
Tactic: rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
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 (a_3 : β) ↦ Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_3) (seq i)) x} x}
    a_1
Tactic: filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ Monotone (f (a, c))) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_3) (seq i)) x}
            x}
      a_1
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
have h₁ : ∀ (a_1 : β), Monotone (f (a, a_1)) → Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
Tactic: filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), f (a, a_1) (seq i) ≤ 1
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ ∀ (q : ℚ), f (a, c) q ≤ 1) x} x →
        Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ ∀ (i : ℕ), f (a, a_3) (seq i) ≤ 1) x} x}
    a_1
Tactic: filter_upwards [hf.le_one a] with c hc using fun i ↦ hc (seq i)
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ ∀ (q : ℚ), f (a, c) q ≤ 1) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ ∀ (i : ℕ), f (a, a_3) (seq i) ≤ 1) x} x}
      a_1
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), f (a, a_1) (seq i) ≤ 1
have h₁ : ∀ (a_1 : β), (∀ (q : ℚ), f (a, a_1) q ≤ 1) → ∀ (i : ℕ), f (a, a_1) (seq i) ≤ 1
Tactic: filter_upwards [hf.le_one a] with c hc using fun i ↦ hc (seq i)