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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
hl : f.length (s i) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
rw : ⨅ (a : R), ⨅ (b : R), ⨅ (_ : s i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
| f.length (s i) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
lhs
      rw [length_eq]

Premises used: StieltjesFunction.length_eq
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
hl : f.length (s i) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ⨅ (a : R), ⨅ (b : R), ⨅ (_ : s i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) <
    f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
conv at hl =>
      lhs
      rw [length_eq]

Premises used: StieltjesFunction.length_eq
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
hl :
  ⨅ (a : R), ⨅ (b : R), ⨅ (_ : s i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) <
    f.length (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (i_1 : R) (i_2 : R),
    s i \ botSet ⊆ Ioc i_1 i_2 ∧ ofReal ((↑f : R → ℝ) i_2 - (↑f : R → ℝ) i_1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
simp only [iInf_lt_iff, exists_prop] at hl

Premises used: exists_prop, iInf_lt_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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
hl :
  ∃ (i_1 : R) (i_2 : R),
    s i \ botSet ⊆ Ioc i_1 i_2 ∧ ofReal ((↑f : R → ℝ) i_2 - (↑f : R → ℝ) i_1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
rcases :
  ∀ (p q' : R) (spq : s i \ botSet ⊆ Ioc p q')
    (hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)),
    ∃ (p : R × R),
      Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (p : R × R),
    Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
rcases hl with ⟨p, q', spq, hq'⟩
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
x : R
hx : x ∈ Icc a' b
h'x : x ∈ s i
a₁ : x ∈ s i \ botSet
⊢ x ∈ Ioc p q'

Tactic:
apply spq
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
x : R
hx : x ∈ Icc a' b
h'x : x ∈ s i
⊢ x ∈ s i \ botSet

Tactic:
simp [h'x, notMem_botSet_of_lt (aa'.trans_le hx.1)]

Premises used: And.left, LT.lt.trans_le, notMem_botSet_of_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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ Icc a' b ∩ s i ⊆ Ioc p q'

Tactic:
have A : Icc a' b ∩ s i ⊆ Ioc p q' := by
      rintro x ⟨hx, h'x⟩
      apply spq
      simp [h'x, notMem_botSet_of_lt (aa'.trans_le hx.1)]
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
pos :
  ∀ (htq' : IsTop q'),
    ∃ (p : R × R),
      Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
neg :
  ∀ (htq' : ¬IsTop q'),
    ∃ (p : R × R),
      Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (p : R × R),
    Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
by_cases htq' : IsTop q'

Premises used: IsTop
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : IsTop q'
⊢ ∃ (p : R × R),
    Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
⟨(p, q'), ?_, hq'⟩

Premises used: Prod.mk, And.intro, Exists.intro
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : IsTop q'
pos : Icc a' b ∩ s i ⊆ Iotop (p, q').1 (p, q').2
⊢ ∃ (p : R × R),
    Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
refine ⟨(p, q'), ?_, hq'⟩
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : IsTop q'
x : R
hx : x ∈ Icc a' b ∩ s i
pos : p < x ∧ x ≤ q'
⊢ x ∈ Iotop (p, q').1 (p, q').2

Tactic:
simp only [Iotop, htq', ↓reduceIte, mem_Ioc]

Premises used: Iotop, reduceIte, Set.mem_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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : IsTop q'
x : R
hx : x ∈ Icc a' b ∩ s i
⊢ p < x ∧ x ≤ q'

Tactic:
⟨(A hx).1, htq' _⟩

Premises used: And.left, And.intro
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : IsTop q'
x : R
hx : x ∈ Icc a' b ∩ s i
⊢ p < x ∧ x ≤ q'

Tactic:
exact ⟨(A hx).1, htq' _⟩
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
⊢ (𝓝[>] q').NeBot

Tactic:
simp [Filter.neBot_iff, nhdsGT_eq_bot_iff, htq', not_covBy]

Premises used: not_covBy, Filter.neBot_iff, nhdsGT_eq_bot_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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
⊢ (𝓝[>] q').NeBot

Tactic:
have : (𝓝[>] q').NeBot := by simp [Filter.neBot_iff, nhdsGT_eq_bot_iff, htq', not_covBy]
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this : (𝓝[>] q').NeBot
apply : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) p) (Ioi q') q'
⊢ ContinuousWithinAt (Y := ℝ≥0∞) (fun (r : R) ↦ ofReal ((↑f : R → ℝ) r - (↑f : R → ℝ) p)) (Ioi q') q'

Tactic:
apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt

Premises used: ENNReal.continuous_ofReal, Continuous.continuousAt, ContinuousAt.comp_continuousWithinAt
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this : (𝓝[>] q').NeBot
⊢ ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) p) (Ioi q') q'

Tactic:
ContinuousWithinAt.sub ?_ continuousWithinAt_const

Premises used: ContinuousWithinAt.sub, continuousWithinAt_const
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this : (𝓝[>] q').NeBot
refine : ContinuousWithinAt (↑f : R → ℝ) (Ioi q') q'
⊢ ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) p) (Ioi q') q'

Tactic:
refine ContinuousWithinAt.sub ?_ continuousWithinAt_const

Premises used: ContinuousWithinAt.sub, continuousWithinAt_const
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this : (𝓝[>] q').NeBot
⊢ ContinuousWithinAt (↑f : R → ℝ) (Ioi q') q'

Tactic:
(f.right_continuous q').mono Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, ContinuousWithinAt.mono, StieltjesFunction.right_continuous
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this : (𝓝[>] q').NeBot
⊢ ContinuousWithinAt (↑f : R → ℝ) (Ioi q') q'

Tactic:
exact (f.right_continuous q').mono Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, ContinuousWithinAt.mono, StieltjesFunction.right_continuous
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this : (𝓝[>] q').NeBot
⊢ ContinuousWithinAt (Y := ℝ≥0∞) (fun (r : R) ↦ ofReal ((↑f : R → ℝ) r - (↑f : R → ℝ) p)) (Ioi q') q'

Tactic:
have : ContinuousWithinAt (fun r => ofReal (f r - f p)) (Ioi q') q' := by
      apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
      refine ContinuousWithinAt.sub ?_ continuousWithinAt_const
      exact (f.right_continuous q').mono Ioi_subset_Ici_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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this_2 : (𝓝[>] q').NeBot
this : ContinuousWithinAt (Y := ℝ≥0∞) (fun (r : R) ↦ ofReal ((↑f : R → ℝ) r - (↑f : R → ℝ) p)) (Ioi q') q'
neg :
  ∀ (q : R) (hq : ofReal ((↑f : R → ℝ) q - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)) (q'q : q' < q),
    ∃ (p : R × R),
      Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
⊢ ∃ (p : R × R),
    Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
rcases (((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩

Premises used: tendsto_order, Filter.Eventually.and, Filter.Eventually.exists, And.right, self_mem_nhdsWithin, Iff.mp
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this_2 : (𝓝[>] q').NeBot
this : ContinuousWithinAt (Y := ℝ≥0∞) (fun (r : R) ↦ ofReal ((↑f : R → ℝ) r - (↑f : R → ℝ) p)) (Ioi q') q'
q : R
hq : ofReal ((↑f : R → ℝ) q - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
q'q : q' < q
⊢ ∃ (p : R × R),
    Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
⟨⟨p, q⟩, A.trans ((Ioc_subset_Ioo_right q'q).trans Ioo_subset_Iotop), hq⟩

Premises used: HasSubset.Subset.trans, Prod.mk, Set.Ioc_subset_Ioo_right, And.intro, Exists.intro, Ioo_subset_Iotop
-- 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 : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ (i : ℕ), s i
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < (↑δ : ℝ≥0∞)
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)
a' : R
ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)
aa' : a < a'
this_1 : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal ((↑f : R → ℝ) q' - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this_2 : (𝓝[>] q').NeBot
this : ContinuousWithinAt (Y := ℝ≥0∞) (fun (r : R) ↦ ofReal ((↑f : R → ℝ) r - (↑f : R → ℝ) p)) (Ioi q') q'
q : R
hq : ofReal ((↑f : R → ℝ) q - (↑f : R → ℝ) p) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
q'q : q' < q
⊢ ∃ (p : R × R),
    Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧ ofReal ((↑f : R → ℝ) p.2 - (↑f : R → ℝ) p.1) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
exact ⟨⟨p, q⟩, A.trans ((Ioc_subset_Ioo_right q'q).trans Ioo_subset_Iotop), hq⟩