awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
inr :
  Tendsto (fun (x_1 : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc x_1 x)) atBot
    (𝓝 (ofReal ((↑f : R → ℝ) x - l)))
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)

Tactic:
refine tendsto_nhds_unique (tendsto_measure_Ioc_atBot _ _) ?_

Premises used: MeasureTheory.tendsto_measure_Ioc_atBot, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
inr : Tendsto (fun (x_1 : R) ↦ ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) x_1)) atBot (𝓝 (ofReal ((↑f : R → ℝ) x - l)))
⊢ Tendsto (fun (x_1 : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc x_1 x)) atBot
    (𝓝 (ofReal ((↑f : R → ℝ) x - l)))

Tactic:
simp_rw [measure_Ioc]

Premises used: StieltjesFunction.measure_Ioc
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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) ↦ ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) x_1)) atBot (𝓝 (ofReal ((↑f : R → ℝ) x - l)))

Tactic:
ENNReal.tendsto_ofReal (Tendsto.const_sub _ hf)

Premises used: Filter.Tendsto.const_sub, ENNReal.tendsto_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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) ↦ ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) x_1)) atBot (𝓝 (ofReal ((↑f : R → ℝ) x - l)))

Tactic:
exact ENNReal.tendsto_ofReal (Tendsto.const_sub _ hf)

Premises used: Filter.Tendsto.const_sub, ENNReal.tendsto_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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∞)
rw₂ : {x} ⊆ Iic x
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio 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)]

Premises used: Iff.mpr, le_rfl, StieltjesFunction.mono', StieltjesFunction.measure_singleton, MeasureTheory.nullMeasurableSet_singleton, Set.Iic_diff_right, MeasureTheory.measure_diff, ENNReal.ofReal_sub, Monotone.leftLim_le, StieltjesFunction.measure_Iic, sub_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ ofReal ((↑f : R → ℝ) x - l - ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) x)) = ofReal (leftLim (↑f : R → ℝ) x - l)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ {x} ⊆ Iic x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ Nonempty R

Tactic:
have : Nonempty R := ⟨x⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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)
inr : NoTopOrder 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)

Tactic:
cases topOrderOrNoTopOrder R

Premises used: topOrderOrNoTopOrder
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ Ici x = Icc x ⊤

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ Ici x = Icc x ⊤

Tactic:
have : Ici x = Icc x ⊤ := by simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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 ⊤
⊢ Tendsto (↑f : R → ℝ) (pure ⊤) (𝓝 l)

Tactic:
rw [atTop_eq_pure_of_isTop isTop_top] at hf

Premises used: Filter.atTop_eq_pure_of_isTop, isTop_top
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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 ⊤
hf₁ : Tendsto (↑f : R → ℝ) (pure ⊤) (𝓝 l)
⊢ Ici x = Icc x ⊤

Tactic:
rw [atTop_eq_pure_of_isTop isTop_top] at hf

Premises used: Filter.atTop_eq_pure_of_isTop, isTop_top
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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)
inl₂ inl₃ : ofReal ((↑f : R → ℝ) ⊤ - leftLim (↑f : R → ℝ) x) = ofReal ((↑f : R → ℝ) ⊤ - leftLim (↑f : R → ℝ) x)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)

Tactic:
rw [this, measure_Icc, tendsto_nhds_unique hf (tendsto_pure_nhds f ⊤)]

Premises used: StieltjesFunction.toFun, tendsto_pure_nhds, StieltjesFunction.measure_Icc, Top.top, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ NoMaxOrder R

Tactic:
have : NoMaxOrder R := NoTopOrder.to_noMaxOrder R
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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)

Tactic:
tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) ?_

Premises used: MeasureTheory.tendsto_measure_Ico_atTop, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
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)))
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) = ofReal (l - leftLim (↑f : R → ℝ) x)

Tactic:
refine tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) ?_

Premises used: MeasureTheory.tendsto_measure_Ico_atTop, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
inr :
  Tendsto (fun (x_1 : R) ↦ ofReal (leftLim (↑f : R → ℝ) x_1 - leftLim (↑f : R → ℝ) x)) atTop
    (𝓝 (ofReal (l - leftLim (↑f : R → ℝ) x)))
⊢ 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:
simp_rw [measure_Ico]

Premises used: StieltjesFunction.measure_Ico
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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) ↦ ofReal (leftLim (↑f : R → ℝ) x_1 - leftLim (↑f : R → ℝ) x)) atTop
    (𝓝 (ofReal (l - leftLim (↑f : R → ℝ) x)))

Tactic:
ENNReal.tendsto_ofReal (Tendsto.sub_const (tendsto_leftLim_atTop_of_tendsto hf) _)

Premises used: Filter.Tendsto.sub_const, ENNReal.tendsto_ofReal, tendsto_leftLim_atTop_of_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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) ↦ ofReal (leftLim (↑f : R → ℝ) x_1 - leftLim (↑f : R → ℝ) x)) atTop
    (𝓝 (ofReal (l - leftLim (↑f : R → ℝ) x)))

Tactic:
exact ENNReal.tendsto_ofReal (Tendsto.sub_const (tendsto_leftLim_atTop_of_tendsto hf) _)

Premises used: Filter.Tendsto.sub_const, ENNReal.tendsto_ofReal, tendsto_leftLim_atTop_of_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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∞)
rw₂ : {x} ⊆ Ici x
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi 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)]

Premises used: Iff.mpr, le_rfl, StieltjesFunction.mono', StieltjesFunction.measure_singleton, MeasureTheory.nullMeasurableSet_singleton, StieltjesFunction.measure_Ici, MeasureTheory.measure_diff, ENNReal.ofReal_sub, Monotone.leftLim_le, Set.Ici_diff_left, sub_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ ofReal (l - leftLim (↑f : R → ℝ) x - ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) x)) = ofReal (l - (↑f : R → ℝ) x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ Ne (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) {x} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ {x} ⊆ Ici x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ Nonempty R

Tactic:
have : Nonempty R := ⟨x⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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∞)

Tactic:
ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_

Premises used: ENNReal.eq_top_of_forall_nnreal_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
refine : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi x) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_

Premises used: ENNReal.eq_top_of_forall_nnreal_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
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)
⊢ (↑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))

Premises used: StieltjesFunction.toFun, Filter.tendsto_atTop, HAdd.hAdd, Iff.mp, Filter.eventually_atTop, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
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:
exact (f.measure_Ioc x (max x N) ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
    le_tsub_of_add_le_right <| hN _ (le_max_right x N))).trans (measure_mono Ioc_subset_Ioi_self)
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
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∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ici x) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf x]

Premises used: StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop, top_le_iff
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ 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:
measure_mono Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ 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:
exact measure_mono Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
⊢ Nonempty R

Tactic:
have : Nonempty R := ⟨x⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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∞)

Tactic:
ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_

Premises used: ENNReal.eq_top_of_forall_nnreal_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
refine : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_

Premises used: ENNReal.eq_top_of_forall_nnreal_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
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)
⊢ (↑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))

Premises used: HSub.hSub, StieltjesFunction.toFun, Filter.tendsto_atBot, Iff.mp, NNReal.toReal, Filter.eventually_atBot
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
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:
exact (f.measure_Ioc (min x N) x ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
    le_sub_comm.mp <| hN _ (min_le_right x N))).trans (measure_mono Ioc_subset_Iic_self)