awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
⊢ Tendsto (fun (x_1 : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc x_1 x)) atBot
    (𝓝 (ofReal ((↑f : R → ℝ) x - l)))
have inr : Tendsto (fun (x_1 : R) ↦ ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) x_1)) atBot (𝓝 (ofReal ((↑f : R → ℝ) x - l)))
Tactic: simp_rw [measure_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) = ofReal (leftLim (↑f : R → ℝ) x - l)
have this : Nonempty R
Tactic: have : Nonempty R := ⟨x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this : Nonempty R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) = ofReal (leftLim (↑f : R → ℝ) x - l)
have rw : ofReal ((↑f : R → ℝ) x - l - ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) x)) = ofReal (leftLim (↑f : R → ℝ) x - l)
Tactic: rw [← Iic_diff_right, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton,
    f.measure_Iic hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this : Nonempty R
rw : ofReal ((↑f : R → ℝ) x - l - ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) x)) = ofReal (leftLim (↑f : R → ℝ) x - l)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) = ofReal (leftLim (↑f : R → ℝ) x - l)
have rw₁ : Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Iic_diff_right, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton,
    f.measure_Iic hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this : Nonempty R
rw : ofReal ((↑f : R → ℝ) x - l - ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) x)) = ofReal (leftLim (↑f : R → ℝ) x - l)
rw₁ : Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) = ofReal (leftLim (↑f : R → ℝ) x - l)
have rw₂ : {x} ⊆ Iic x
Tactic: rw [← Iic_diff_right, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton,
    f.measure_Iic hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have this : Nonempty R
Tactic: have : Nonempty R := ⟨x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
this : Nonempty R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have inl : ∀ (val : OrderTop R), ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
Tactic: cases topOrderOrNoTopOrder R
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
this : Nonempty R
inl : ∀ (val : OrderTop R), ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have inr : NoTopOrder R → ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
Tactic: cases topOrderOrNoTopOrder R
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
this : Nonempty R
val : OrderTop R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have this₁ : Ici x = Icc x ⊤
Tactic: have : Ici x = Icc x ⊤ := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
this_1 : Nonempty R
val : OrderTop R
this : Ici x = Icc x ⊤
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have hf₁ : Tendsto (↑f : R → ℝ) (pure ⊤) (𝓝 l)
Tactic: rw [atTop_eq_pure_of_isTop isTop_top] at hf
Cleared hypotheses: hf, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
x : R
this_1 : Nonempty R
val : OrderTop R
hf : Tendsto (↑f : R → ℝ) (pure ⊤) (𝓝 l)
this : Ici x = Icc x ⊤
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have inl : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc x ⊤) = ofReal (l - leftLim (↑f : R → ℝ) x)
Tactic: rw [this, measure_Icc, tendsto_nhds_unique hf (tendsto_pure_nhds f ⊤)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
x : R
this_1 : Nonempty R
val : OrderTop R
hf : Tendsto (↑f : R → ℝ) (pure ⊤) (𝓝 l)
this : Ici x = Icc x ⊤
inl : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc x ⊤) = ofReal (l - leftLim (↑f : R → ℝ) x)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have inl₁ : ofReal ((↑f : R → ℝ) ⊤ - leftLim (↑f : R → ℝ) x) = ofReal (l - leftLim (↑f : R → ℝ) x)
Tactic: rw [this, measure_Icc, tendsto_nhds_unique hf (tendsto_pure_nhds f ⊤)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
x : R
this_1 : Nonempty R
val : OrderTop R
hf : Tendsto (↑f : R → ℝ) (pure ⊤) (𝓝 l)
this : Ici x = Icc x ⊤
inl : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc x ⊤) = ofReal (l - leftLim (↑f : R → ℝ) x)
inl₁ : ofReal ((↑f : R → ℝ) ⊤ - leftLim (↑f : R → ℝ) x) = ofReal (l - leftLim (↑f : R → ℝ) x)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have inl₂ : ofReal ((↑f : R → ℝ) ⊤ - leftLim (↑f : R → ℝ) x) = ofReal ((↑f : R → ℝ) ⊤ - leftLim (↑f : R → ℝ) x)
Tactic: rw [this, measure_Icc, tendsto_nhds_unique hf (tendsto_pure_nhds f ⊤)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
this : Nonempty R
val : NoTopOrder R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have this₁ : NoMaxOrder R
Tactic: have : NoMaxOrder R := NoTopOrder.to_noMaxOrder R
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
this_1 : Nonempty R
val : NoTopOrder R
this : NoMaxOrder R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)
have inr : Tendsto (fun (x_1 : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico x x_1)) atTop
  (𝓝 (ofReal (l - leftLim (↑f : R → ℝ) x)))
Tactic: refine tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
this_1 : Nonempty R
val : NoTopOrder R
this : NoMaxOrder R
⊢ Tendsto (fun (x_1 : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico x x_1)) atTop
    (𝓝 (ofReal (l - leftLim (↑f : R → ℝ) x)))
have inr : Tendsto (fun (x_1 : R) ↦ ofReal (leftLim (↑f : R → ℝ) x_1 - leftLim (↑f : R → ℝ) x)) atTop
  (𝓝 (ofReal (l - leftLim (↑f : R → ℝ) x)))
Tactic: simp_rw [measure_Ico]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x) = ofReal (l - (↑f : R → ℝ) x)
have rw : ofReal (l - leftLim (↑f : R → ℝ) x - ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) x)) = ofReal (l - (↑f : R → ℝ) x)
Tactic: rw [← Ici_diff_left, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton,
    f.measure_Ici hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
rw : ofReal (l - leftLim (↑f : R → ℝ) x - ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) x)) = ofReal (l - (↑f : R → ℝ) x)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x) = ofReal (l - (↑f : R → ℝ) x)
have rw₁ : Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Ici_diff_left, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton,
    f.measure_Ici hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atTop (𝓝 l)
x : R
rw : ofReal (l - leftLim (↑f : R → ℝ) x - ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) x)) = ofReal (l - (↑f : R → ℝ) x)
rw₁ : Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x) = ofReal (l - (↑f : R → ℝ) x)
have rw₂ : {x} ⊆ Ici x
Tactic: rw [← Ici_diff_left, measure_diff _ (nullMeasurableSet_singleton x), measure_singleton,
    f.measure_Ici hf, ← ofReal_sub _ (sub_nonneg.mpr <| Monotone.leftLim_le f.mono' le_rfl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atTop atTop
x : R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : Nonempty R
Tactic: have : Nonempty R := ⟨x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atTop atTop
x : R
this : Nonempty R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x)
Tactic: refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atTop atTop
x : R
this : Nonempty R
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≤ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x)
have obtain : ∀ (N : R) (hN : ∀ b ≥ N, (↑r : ℝ) + (↑f : R → ℝ) x ≤ (↑f : R → ℝ) b),
  (↑r : ℝ≥0∞) ≤ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x)
Tactic: obtain ⟨N, hN⟩ := eventually_atTop.mp (tendsto_atTop.mp hf (r + f x))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atTop atTop
x : R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x) : ℝ≥0∞)
  (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) : ℝ≥0∞)
Tactic: rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : Nonempty R
Tactic: have : Nonempty R := ⟨x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this : Nonempty R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x)
Tactic: refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this : Nonempty R
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≤ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x)
have obtain : ∀ (N : R) (hN : ∀ b ≤ N, (↑f : R → ℝ) b ≤ (↑f : R → ℝ) x - (↑r : ℝ)),
  (↑r : ℝ≥0∞) ≤ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x)
Tactic: obtain ⟨N, hN⟩ := eventually_atBot.mp (tendsto_atBot.mp hf (f x - r))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : Nonempty R
Tactic: have : Nonempty R := ⟨x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this : Nonempty R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have inl : ∀ (val : OrderBot R), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: cases botOrderOrNoBotOrder R
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this : Nonempty R
inl : ∀ (val : OrderBot R), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have inr : NoBotOrder R → Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: cases botOrderOrNoBotOrder R
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this : Nonempty R
val : OrderBot R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hf₁ : Tendsto (↑f : R → ℝ) (pure ⊥) atBot
Tactic: rw [atBot_eq_pure_of_isBot isBot_bot] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this : Nonempty R
val : NoBotOrder R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have this₁ : NoMinOrder R
Tactic: have : NoMinOrder R := NoBotOrder.to_noMinOrder R
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have inr : ∀ (y : R) (hy : y < x), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
y : R
hy : y < x
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)
have inr : LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic y) : ℝ≥0∞)
  (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞)
Tactic: rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
inst_8 : Nonempty R
l u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ = ofReal (u - l)
have refine : Tendsto (fun (x : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x)) atTop (𝓝 (ofReal (u - l)))
Tactic: refine tendsto_nhds_unique (tendsto_measure_Iic_atTop _) ?_