awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
hqs_tendsto : Tendsto qs atBot atBot
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atBot (𝓝 0)
have refine : ∀ (x : ℝ), (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ (f a ∘ qs) x
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    ((hf.tendsto_atBot_zero a).comp hqs_tendsto) (stieltjesFunction_nonneg hf a) fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ (f a ∘ qs) x
have rw : (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(qs x) : ℝ)
Tactic: rw [Function.comp_apply, ← stieltjesFunction_eq hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atTop (𝓝 1)
have h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
Tactic: have h_exists : ∀ x : ℝ, ∃ q : ℚ, x - 1 < q ∧ ↑q < x := fun x ↦ exists_rat_btwn (sub_one_lt x)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
⊢ Tendsto qs atTop atTop
have rw : ∀ (b : ℚ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ qs a
Tactic: rw [tendsto_atTop_atTop]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
⊢ ∀ (b : ℚ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ qs a
have refine : ∀ (q : ℚ) (y : ℝ) (hy : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ y), q ≤ qs y
Tactic: refine fun q ↦ ⟨q + 1, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
q : ℚ
y : ℝ
hy : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ y
⊢ q ≤ qs y
have h_le : y - 1 ≤ (↑(qs y) : ℝ)
Tactic: have h_le : y - 1 ≤ qs y := (h_exists y).choose_spec.1.le
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
q : ℚ
y : ℝ
hy : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ y
h_le : y - 1 ≤ (↑(qs y) : ℝ)
⊢ q ≤ qs y
have h_le₁ : y ≤ HAdd.hAdd (α := ℝ) (↑(qs y) : ℝ) 1
Tactic: rw [sub_le_iff_le_add] at h_le
Cleared hypotheses: h_le
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atTop (𝓝 1)
have hqs_tendsto : Tendsto qs atTop atTop
Tactic: have hqs_tendsto : Tendsto qs atTop atTop := by
    rw [tendsto_atTop_atTop]
    refine fun q ↦ ⟨q + 1, fun y hy ↦ ?_⟩
    have h_le : y - 1 ≤ qs y := (h_exists y).choose_spec.1.le
    rw [sub_le_iff_le_add] at h_le
    exact_mod_cast le_of_add_le_add_right (hy.trans h_le)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
hqs_tendsto : Tendsto qs atTop atTop
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atTop (𝓝 1)
have refine : f a ∘ qs ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le ((hf.tendsto_atTop_one a).comp hqs_tendsto)
      tendsto_const_nhds ?_ (stieltjesFunction_le_one hf a)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ (f a ∘ qs) x ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x
have rw : (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(qs x) : ℝ) ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x
Tactic: rw [Function.comp_apply, ← stieltjesFunction_eq hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ) (fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x) fun (a : α) ↦
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
have h : ∀ (a : α), (↑(hf.stieltjesFunction a) : ℝ → ℝ) x = ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x = ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
have h : Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
  (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))
Tactic: rw [← StieltjesFunction.iInf_rat_gt_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
⊢ Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))
have h : ∀ (q : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑q : ℚ) : ℝ) = f a (↑q : ℚ)
Tactic: congr with q
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
q : { r' : ℚ // x < (↑r' : ℝ) }
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑q : ℚ) : ℝ) = f a (↑q : ℚ)
have h : f a (↑q : ℚ) = f a (↑q : ℚ)
Tactic: rw [stieltjesFunction_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
⊢ Measurable (β := ℝ) fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x
have this : Eq.{u_1 + 1} (α := (a : α) → ℝ) (fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x) fun (a : α) ↦
  ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
Tactic: have : (fun a ↦ hf.stieltjesFunction a x) = fun a ↦ ⨅ r : { r' : ℚ // x < r' }, f a ↑r := by
    ext1 a
    rw [← StieltjesFunction.iInf_rat_gt_eq]
    congr with q
    rw [stieltjesFunction_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ) (fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x) fun (a : α) ↦
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
⊢ Measurable (β := ℝ) fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x
have rw : Measurable (β := ℝ) fun (a : α) ↦ ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
    ENNReal.ofReal ((↑(hf.stieltjesFunction a) : ℝ → ℝ) x)
have rw : ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
  ENNReal.ofReal ((↑(hf.stieltjesFunction a) : ℝ → ℝ) x - 0)
Tactic: rw [← sub_zero (hf.stieltjesFunction a x)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ Eq (α := ℝ≥0∞) (((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) univ = ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0)
Tactic: rw [← ENNReal.ofReal_one, ← sub_zero (1 : ℝ)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
⊢ stieltjesOfMeasurableRat (fun (p : Unit × α) ↦ f p.2) ⋯ ((), a) = stieltjesOfMeasurableRat f hf a
have simp_rw : Eq (α := StieltjesFunction ℝ)
  { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun (p : Unit × α) ↦ f p.2) ((), a), mono' := sorry,
    right_continuous' := sorry }
  { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ toRatCDF f p.2) ((), a), mono' := sorry,
    right_continuous' := sorry }
Tactic: simp_rw [stieltjesOfMeasurableRat, IsMeasurableRatCDF.stieltjesFunction,
    ← IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod a]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
⊢ Eq (α := StieltjesFunction ℝ)
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun (p : Unit × α) ↦ f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ toRatCDF f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }
have e_toFun : ∀ (x : ℝ),
  IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun (p : Unit × α) ↦ f p.2) ((), a) x =
    IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ toRatCDF f p.2) ((), a) x
Tactic: congr 1 with x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
⊢ IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun (p : Unit × α) ↦ f p.2) ((), a) x =
    IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ toRatCDF f p.2) ((), a) x
have e_toFun : ∀ (p : Unit × α), toRatCDF (fun (p : Unit × α) ↦ f p.2) p = toRatCDF f p.2
Tactic: congr 1 with p : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
fst : Unit
b : α
⊢ toRatCDF (fun (p : Unit × α) ↦ f p.2) (fst, b) = toRatCDF f (fst, b).2
have e_toFun : toRatCDF (fun (p : Unit × α) ↦ f p.2) (fst, b) = toRatCDF (fun (p : Unit × α) ↦ f p.2) ((), b)
Tactic: rw [← toRatCDF_unit_prod b]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
p : Unit × α
⊢ toRatCDF (fun (p : Unit × α) ↦ f p.2) p = toRatCDF f p.2
have e_toFun : ∀ (fst : Unit) (b : α), toRatCDF (fun (p : Unit × α) ↦ f p.2) (fst, b) = toRatCDF f (fst, b).2
Tactic: cases p with
  | mk _ b => rw [← toRatCDF_unit_prod b]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop (𝓝 0)
have refine_1 : Antitone s'
Tactic: refine tendsto_integral_density_of_antitone le_rfl a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
refine_1 : Antitone s'
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop (𝓝 0)
have refine_2 : Eq (α := Set ℝ) (⋂ (i : ℕ), s' i) ∅
Tactic: refine tendsto_integral_density_of_antitone le_rfl a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Antitone s'
have refine_1 : ∀ (i j : ℕ) (hij : i ≤ j), LE.le (α := ℝ) (↑(s j) : ℝ) (↑(s i) : ℝ)
Tactic: refine fun i j hij ↦ Iic_subset_Iic.mpr ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Eq (α := Set ℝ) (⋂ (i : ℕ), s' i) ∅
have refine_2 : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), s' i) x ↔ Membership.mem (γ := Set ℝ) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), s' i) x ↔ Membership.mem (γ := Set ℝ) ∅ x
have refine_2 : ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
Tactic: simp only [mem_iInter, mem_Iic, mem_empty_iff_false, iff_false, not_forall, not_le, s']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
have refine_2 : ∀ (hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b) (x : ℝ), ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
Tactic: rw [tendsto_atTop_atBot] at hs_tendsto
Cleared hypotheses: hs_tendsto, s', x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
have refine_2 : ∀ (q : ℚ) (hq : (↑q : ℝ) < x), ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
Tactic: have ⟨q, hq⟩ := exists_rat_lt x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : (↑q : ℝ) < x
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
have refine_2 : ∀ (i : ℕ) (hi : ∀ (a : ℕ), i ≤ a → s a ≤ q), ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
Tactic: obtain ⟨i, hi⟩ := hs_tendsto q
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : (↑q : ℝ) < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
have refine_2 : LE.le (α := ℝ) (↑(s i) : ℝ) (↑q : ℝ)
Tactic: refine ⟨i, lt_of_le_of_lt ?_ hq⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop (𝓝 (Measure.real.{u_3} (α := γ) (m := mγ) ((κ.fst : (a : α) → Measure γ) a) univ))
have rw : Tendsto
  (fun (m : ℕ) ↦
    @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
      κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
  atTop
  (𝓝
    (Measure.real.{u_3} (α := γ × ℝ) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × ℝ)) a)
      {p : γ × ℝ | Membership.mem (γ := Set γ) univ p.1}))
Tactic: rw [fst_real_apply _ _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop
    (𝓝
      (Measure.real.{u_3} (α := γ × ℝ) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × ℝ)) a)
        {p : γ × ℝ | Membership.mem (γ := Set γ) univ p.1}))
have refine_1 : Monotone s'
Tactic: refine tendsto_integral_density_of_monotone (le_rfl : fst κ ≤ fst κ)
      a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
refine_1 : Monotone s'
⊢ Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop
    (𝓝
      (Measure.real.{u_3} (α := γ × ℝ) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × ℝ)) a)
        {p : γ × ℝ | Membership.mem (γ := Set γ) univ p.1}))
have refine_2 : Eq (α := Set ℝ) (⋃ (i : ℕ), s' i) univ
Tactic: refine tendsto_integral_density_of_monotone (le_rfl : fst κ ≤ fst κ)
      a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Eq (α := Set ℝ) (⋃ (i : ℕ), s' i) univ
have refine_2 : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (⋃ (i : ℕ), s' i) x ↔ Membership.mem (γ := Set ℝ) univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (⋃ (i : ℕ), s' i) x ↔ Membership.mem (γ := Set ℝ) univ x
have refine_2 : ∃ (i : ℕ), x ∈ s' i
Tactic: simp only [mem_iUnion, mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
⊢ ∃ (i : ℕ), x ∈ s' i
have refine_2 : ∀ (hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a),
  let s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ);
  ∀ (x : ℝ), ∃ (i : ℕ), x ∈ s' i
Tactic: rw [tendsto_atTop_atTop] at hs_tendsto
Cleared hypotheses: hs_tendsto, s', x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
⊢ ∃ (i : ℕ), x ∈ s' i
have refine_2 : ∀ (q : ℚ) (hq : x < (↑q : ℝ)), ∃ (i : ℕ), x ∈ s' i
Tactic: have ⟨q, hq⟩ := exists_rat_gt x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : x < (↑q : ℝ)
⊢ ∃ (i : ℕ), x ∈ s' i
have refine_2 : ∀ (i : ℕ) (hi : ∀ (a : ℕ), i ≤ a → q ≤ s a), ∃ (i : ℕ), x ∈ s' i
Tactic: obtain ⟨i, hi⟩ := hs_tendsto q
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : x < (↑q : ℝ)
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → q ≤ s a
⊢ ∃ (i : ℕ), x ∈ s' i
have refine_2 : LE.le (α := ℝ) (↑q : ℝ) (↑(s i) : ℝ)
Tactic: refine ⟨i, hq.le.trans ?_⟩