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
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∞)
inr : NoBotOrder 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∞)

Tactic:
cases botOrderOrNoBotOrder R

Premises used: botOrderOrNoBotOrder
-- 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
val : OrderBot R
⊢ Tendsto (↑f : R → ℝ) (pure ⊥) atBot

Tactic:
rw [atBot_eq_pure_of_isBot isBot_bot] at hf

Premises used: Filter.atBot_eq_pure_of_isBot, isBot_bot
-- 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
x : R
this : Nonempty R
val : OrderBot R
hf : Tendsto (↑f : R → ℝ) (pure ⊥) atBot
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa using (tendsto_pure_left.1 hf) _ (Iio_mem_atBot (f ⊥))

Premises used: Filter.tendsto_pure_left, StieltjesFunction.toFun, Bot.bot, Iff.mp, Filter.Iio_mem_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
val : NoBotOrder R
⊢ NoMinOrder R

Tactic:
have : NoMinOrder R := NoBotOrder.to_noMinOrder 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
hf : Tendsto (↑f : R → ℝ) atBot atBot
x : R
this_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
⊢ ∃ (y : R), y < x

Tactic:
exists_lt x

Premises used: NoMinOrder.exists_lt
-- 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_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
inr : ∀ (y : R) (hy : y < x), 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∞)

Tactic:
obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x

Premises used: NoMinOrder.exists_lt
-- 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_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
y : R
hy : y < x
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∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio x) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf y]

Premises used: StieltjesFunction.measure_Iic_of_tendsto_atBot_atBot, 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 → ℝ) atBot atBot
x : R
this_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
y : R
hy : y < x
⊢ 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:
measure_mono <| Set.Iic_subset_Iio.mpr <| hy

Premises used: Iff.mpr, Set.Iic_subset_Iio, 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
this_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
y : R
hy : y < x
⊢ 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:
exact measure_mono <| Set.Iic_subset_Iio.mpr <| hy

Premises used: Iff.mpr, Set.Iic_subset_Iio, 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
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)

Tactic:
tendsto_nhds_unique (tendsto_measure_Iic_atTop _) ?_

Premises used: MeasureTheory.tendsto_measure_Iic_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
inst_8 : Nonempty R
l u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
refine : Tendsto (fun (x : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x)) atTop (𝓝 (ofReal (u - l)))
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ = ofReal (u - l)

Tactic:
refine tendsto_nhds_unique (tendsto_measure_Iic_atTop _) ?_

Premises used: MeasureTheory.tendsto_measure_Iic_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
inst_8 : Nonempty R
l u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
simp_rw : Tendsto (fun (x : R) ↦ ofReal ((↑f : R → ℝ) x - l)) atTop (𝓝 (ofReal (u - l)))
⊢ Tendsto (fun (x : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x)) atTop (𝓝 (ofReal (u - l)))

Tactic:
simp_rw [measure_Iic f hfl]

Premises used: StieltjesFunction.measure_Iic
-- 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
inst_8 : Nonempty R
l u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ Tendsto (fun (x : R) ↦ ofReal ((↑f : R → ℝ) x - l)) atTop (𝓝 (ofReal (u - l)))

Tactic:
ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)

Premises used: Filter.Tendsto.sub_const, 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
inst_8 : Nonempty R
l u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ Tendsto (fun (x : R) ↦ ofReal ((↑f : R → ℝ) x - l)) atTop (𝓝 (ofReal (u - l)))

Tactic:
exact ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)

Premises used: Filter.Tendsto.sub_const, 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atTop atTop
inhabit :
  ∀ (inhabited_h : Inhabited R), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
inhabit 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atTop atTop
inhabited_h : Inhabited R
rw :
  LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi default) : ℝ≥0∞)
    (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

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

Premises used: Inhabited.default, 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atTop atTop
inhabited_h : Inhabited R
⊢ LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi default) : ℝ≥0∞)
    (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
measure_mono (subset_univ _)

Premises used: Set.subset_univ, 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atTop atTop
inhabited_h : Inhabited R
⊢ LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi default) : ℝ≥0∞)
    (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact measure_mono (subset_univ _)

Premises used: Set.subset_univ, 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atBot atBot
inhabit :
  ∀ (inhabited_h : Inhabited R), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
inhabit 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atBot atBot
inhabited_h : Inhabited R
rw :
  LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio default) : ℝ≥0∞)
    (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf default]

Premises used: Inhabited.default, top_le_iff, StieltjesFunction.measure_Iio_of_tendsto_atBot_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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atBot atBot
inhabited_h : Inhabited R
⊢ LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio default) : ℝ≥0∞)
    (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
measure_mono (subset_univ _)

Premises used: Set.subset_univ, 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atBot atBot
inhabited_h : Inhabited R
⊢ LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio default) : ℝ≥0∞)
    (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact measure_mono (subset_univ _)

Premises used: Set.subset_univ, 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
l u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
measure_univ_lt_top : LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (m0 := inst_4) f.measure

Tactic:
constructor
-- 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 u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
measure_univ_lt_top :
  IsEmpty R → LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
measure_univ_lt_top₁ :
  Nonempty R → LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
cases isEmpty_or_nonempty R

Premises used: isEmpty_or_nonempty
-- 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 u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
h : IsEmpty R
⊢ LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [eq_empty_of_isEmpty]

Premises used: Set.eq_empty_of_isEmpty
-- 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 u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
h : Nonempty R
⊢ LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [f.measure_univ hfl hfu]

Premises used: StieltjesFunction.measure_univ
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
inl : IsEmpty R → IsFiniteMeasure (m0 := inst_4) f.measure
inr : Nonempty R → IsFiniteMeasure (m0 := inst_4) f.measure
⊢ IsFiniteMeasure (m0 := inst_4) f.measure

Tactic:
cases isEmpty_or_nonempty R

Premises used: isEmpty_or_nonempty
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : IsEmpty R
⊢ IsFiniteMeasure (m0 := inst_4) f.measure

Tactic:
infer_instance
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
inl : ∀ (H : Tendsto (↑f : R → ℝ) atTop atTop), ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
inr : ∀ (H : ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 l)), ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)

Tactic:
rcases tendsto_atTop_of_monotone f.mono with H | H

Premises used: StieltjesFunction.mono, tendsto_atTop_of_monotone
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
H : Tendsto (↑f : R → ℝ) atTop atTop
⊢ ∃ (x : R), C + 1 ≤ (↑f : R → ℝ) x

Tactic:
(tendsto_atTop.1 H (C + 1)).exists

Premises used: Filter.tendsto_atTop, Filter.Eventually.exists, HAdd.hAdd, Iff.mp, OfNat.ofNat
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
H : Tendsto (↑f : R → ℝ) atTop atTop
inl : ∀ (x : R) (hx : C + 1 ≤ (↑f : R → ℝ) x), ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)

Tactic:
obtain ⟨x, hx⟩ : ∃ x, C + 1 ≤ f x := (tendsto_atTop.1 H (C + 1)).exists

Premises used: Filter.tendsto_atTop, Filter.Eventually.exists, HAdd.hAdd, Iff.mp, OfNat.ofNat
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
H : Tendsto (↑f : R → ℝ) atTop atTop
x : R
hx : C + 1 ≤ (↑f : R → ℝ) x
⊢ ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)

Tactic:
grind
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
H : ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 l)
⊢ ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)

Tactic:
H
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
H : ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 l)
⊢ ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)

Tactic:
exact H
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
inr : ∀ (u : ℝ) (hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)), IsFiniteMeasure (m0 := inst_4) f.measure
⊢ IsFiniteMeasure (m0 := inst_4) f.measure

Tactic:
obtain ⟨u, hu⟩ : ∃ u, Tendsto f atTop (𝓝 u) := by
    rcases tendsto_atTop_of_monotone f.mono with H | H
    · obtain ⟨x, hx⟩ : ∃ x, C + 1 ≤ f x := (tendsto_atTop.1 H (C + 1)).exists
      grind
    exact H
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
inl : ∀ (H : Tendsto (↑f : R → ℝ) atBot atBot), ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
inr : ∀ (H : ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)), ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
⊢ ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)

Tactic:
rcases tendsto_atBot_of_monotone f.mono with H | H

Premises used: tendsto_atBot_of_monotone, StieltjesFunction.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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
H : Tendsto (↑f : R → ℝ) atBot atBot
⊢ ∃ (x : R), (↑f : R → ℝ) x ≤ -C - 1

Tactic:
(tendsto_atBot.1 H (-C - 1)).exists

Premises used: HSub.hSub, Filter.Eventually.exists, Filter.tendsto_atBot, Iff.mp, OfNat.ofNat, Neg.neg
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
H : Tendsto (↑f : R → ℝ) atBot atBot
inl : ∀ (x : R) (hx : (↑f : R → ℝ) x ≤ -C - 1), ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
⊢ ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)

Tactic:
obtain ⟨x, hx⟩ : ∃ x, f x ≤ - C - 1 := (tendsto_atBot.1 H (-C - 1)).exists

Premises used: HSub.hSub, Filter.Eventually.exists, Filter.tendsto_atBot, Iff.mp, OfNat.ofNat, Neg.neg