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
a : R
c d : ℕ → R
s_1 s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R),
      Icc a b ⊆ ⋃ i ∈ (↑t : Set ℕ), Iotop (c i) (d i) →
        ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ t, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Iotop (c i) (d i)
⊢ b ∈ Ioc (c i) (d i)

Tactic:
replace bcd : b ∈ Ioc (c i) (d i) := Iotop_subset_Ioc bcd
-- 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
a : R
c d : ℕ → R
s_1 s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R),
      Icc a b ⊆ ⋃ i ∈ (↑t : Set ℕ), Iotop (c i) (d i) →
        ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ t, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
inr :
  ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
    ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i) + ((↑f : R → ℝ) (c i) - (↑f : R → ℝ) a))
inr₁ : Icc a (c i) ⊆ ⋃ i_1 ∈ (↑(s.erase i) : Set ℕ), Iotop (c i_1) (d i_1)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
    ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i)) + ∑ x ∈ s.erase i, ofReal ((↑f : R → ℝ) (d x) - (↑f : R → ℝ) (c x))

Tactic:
grw [← IH _ (Finset.erase_ssubset is) (c i), ← ENNReal.ofReal_add_le]

Premises used: ENNReal.ofReal_add_le, Finset.erase_ssubset
-- 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
a : R
c d : ℕ → R
s_1 s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R),
      Icc a b ⊆ ⋃ i ∈ (↑t : Set ℕ), Iotop (c i) (d i) →
        ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ t, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
inr : (↑f : R → ℝ) b - (↑f : R → ℝ) a ≤ (↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i) + ((↑f : R → ℝ) (c i) - (↑f : R → ℝ) a)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
    ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i) + ((↑f : R → ℝ) (c i) - (↑f : R → ℝ) a))

Tactic:
gcongr
-- 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
a : R
c d : ℕ → R
s_1 s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R),
      Icc a b ⊆ ⋃ i ∈ (↑t : Set ℕ), Iotop (c i) (d i) →
        ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ t, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
inr : (↑f : R → ℝ) b - (↑f : R → ℝ) a ≤ (↑f : R → ℝ) (d i) - (↑f : R → ℝ) a
⊢ (↑f : R → ℝ) b - (↑f : R → ℝ) a ≤ (↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i) + ((↑f : R → ℝ) (c i) - (↑f : R → ℝ) a)

Tactic:
rw [sub_add_sub_cancel]

Premises used: sub_add_sub_cancel
-- 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
a : R
c d : ℕ → R
s_1 s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R),
      Icc a b ⊆ ⋃ i ∈ (↑t : Set ℕ), Iotop (c i) (d i) →
        ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ t, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ (↑f : R → ℝ) b - (↑f : R → ℝ) a ≤ (↑f : R → ℝ) (d i) - (↑f : R → ℝ) a

Tactic:
sub_le_sub_right (f.mono bcd.2) _

Premises used: sub_le_sub_right, StieltjesFunction.mono, And.right
-- 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
a : R
c d : ℕ → R
s_1 s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R),
      Icc a b ⊆ ⋃ i ∈ (↑t : Set ℕ), Iotop (c i) (d i) →
        ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ t, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ (↑f : R → ℝ) b - (↑f : R → ℝ) a ≤ (↑f : R → ℝ) (d i) - (↑f : R → ℝ) a

Tactic:
exact sub_le_sub_right (f.mono bcd.2) _

Premises used: sub_le_sub_right, StieltjesFunction.mono, And.right
-- 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
a : R
c d : ℕ → R
s_1 s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R),
      Icc a b ⊆ ⋃ i ∈ (↑t : Set ℕ), Iotop (c i) (d i) →
        ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ t, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
x : R
h₁ : a ≤ x
h₂ : x ≤ c i
apply : ∀ (h : x ∈ Iotop (c i) (d i)), False
⊢ Membership.mem (γ := Set R) (⋃ i_1 ∈ (↑(s.erase i) : Set ℕ), Iotop (c i_1) (d i_1)) x

Tactic:
apply (cv ⟨h₁, le_trans h₂ (le_of_lt bcd.1)⟩).resolve_left (fun h ↦ ?_)

Premises used: le_of_lt, Or.resolve_left, And.left, And.intro, le_trans
-- 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
a : R
c d : ℕ → R
s_1 s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R),
      Icc a b ⊆ ⋃ i ∈ (↑t : Set ℕ), Iotop (c i) (d i) →
        ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ t, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
x : R
h₁ : a ≤ x
h₂ : x ≤ c i
h : x ∈ Iotop (c i) (d i)
order order₁ order₂ order₃ : ¬False → False
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ : True → False
⊢ False

Tactic:
order [(Iotop_subset_Ioc h).1]

Premises used: And.left, Iotop_subset_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
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
refine_1 : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
refine_2 : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
refine_1 : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) ≤ f.length (Ioc a b)
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
rw [← f.length_Ioc]

Premises used: StieltjesFunction.length_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
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) ≤ f.length (Ioc a b)

Tactic:
apply outer_le_length

Premises used: StieltjesFunction.outer_le_length
-- 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
refine_2 : ∀ (hab : b ≤ a), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)
refine_2₁ : ∀ (hab : a < b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)

Tactic:
rcases le_or_gt b a with hab | hab

Premises used: le_or_gt
-- 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 : b ≤ a
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) = 0

Tactic:
simpa using f.mono hab

Premises used: 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 : DenselyOrdered R
a b : R
hab : b ≤ a
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) = 0

Tactic:
have : ofReal (f b - f a) = 0 := by simpa using f.mono hab
-- 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 : b ≤ a
this : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) = 0
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)

Tactic:
simp [this]
-- 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
apply :
  ∀ (s : ℕ → Set R) (hs : Ioc a b ⊆ ⋃ (i : ℕ), s i) (ε : ℝ≥0) (εpos : 0 < ε)
    (h : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), f.length (s i)) ∞),
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)

Tactic:
apply (le_iInf₂ fun s hs => ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_)

Premises used: le_iInf₂, ENNReal.le_of_forall_pos_le_add
-- 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
⊢ 0 < (↑δ : ℝ≥0∞)

Tactic:
simpa [δ] using εpos.ne'

Premises used: LT.lt.ne'
-- 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
⊢ 0 < (↑δ : ℝ≥0∞)

Tactic:
have δpos : 0 < (δ : ℝ≥0∞) := by simpa [δ] using εpos.ne'
-- 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∞)
rcases :
  ∀ (ε' : ℕ → ℝ≥0) (ε'0 : ∀ (i : ℕ), 0 < ε' i) (hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥0∞)),
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)

Tactic:
rcases ENNReal.exists_pos_sum_of_countable δpos.ne' ℕ with ⟨ε', ε'0, hε⟩

Premises used: LT.lt.ne', ENNReal.exists_pos_sum_of_countable, Nat
-- 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∞)
⊢ ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a

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∞)
refine : ContinuousWithinAt (↑f : R → ℝ) (Ioi a) a
⊢ ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a

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∞)
⊢ ContinuousWithinAt (↑f : R → ℝ) (Ioi a) a

Tactic:
(f.right_continuous a).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∞)
⊢ ContinuousWithinAt (↑f : R → ℝ) (Ioi a) a

Tactic:
exact (f.right_continuous a).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∞)
⊢ ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a

Tactic:
have A : ContinuousWithinAt (fun r => f r - f a) (Ioi a) a := by
      refine ContinuousWithinAt.sub ?_ continuousWithinAt_const
      exact (f.right_continuous a).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 : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a
rwa : 0 < (↑δ : ℝ)
rwa₁ : 0 < δ
rwa₂ rwa₃ rwa₄ rwa₅ : 0 < (↑δ : ℝ≥0∞)
⊢ (↑f : R → ℝ) a - (↑f : R → ℝ) a < (↑δ : ℝ)

Tactic:
rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]

Premises used: sub_self, ENNReal.coe_pos, NNReal.coe_pos
-- 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 : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a
⊢ (↑f : R → ℝ) a - (↑f : R → ℝ) a < (↑δ : ℝ)

Tactic:
have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
-- 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 : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a
B : (↑f : R → ℝ) a - (↑f : R → ℝ) a < (↑δ : ℝ)
⊢ (𝓝[>] a).NeBot

Tactic:
have : (𝓝[>] a).NeBot := nhdsGT_neBot_of_exists_gt ⟨b, hab⟩
-- 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 : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a
B : (↑f : R → ℝ) a - (↑f : R → ℝ) a < (↑δ : ℝ)
this : (𝓝[>] a).NeBot
⊢ ∃ (a' : R), (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ) ∧ a < a'

Tactic:
(((tendsto_order.1 A).2 _ B).and self_mem_nhdsWithin).exists

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 : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a
B : (↑f : R → ℝ) a - (↑f : R → ℝ) a < (↑δ : ℝ)
this : (𝓝[>] a).NeBot
⊢ ∃ (a' : R), (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ) ∧ a < a'

Tactic:
exact (((tendsto_order.1 A).2 _ B).and self_mem_nhdsWithin).exists

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∞)
obtain :
  ∀ (a' : R) (ha' : (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ)) (aa' : a < a'),
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨a', ha', aa'⟩ : ∃ a', f a' - f a < δ ∧ a < a' := by
    have A : ContinuousWithinAt (fun r => f r - f a) (Ioi a) a := by
      refine ContinuousWithinAt.sub ?_ continuousWithinAt_const
      exact (f.right_continuous a).mono Ioi_subset_Ici_self
    have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
    have : (𝓝[>] a).NeBot := nhdsGT_neBot_of_exists_gt ⟨b, hab⟩
    exact (((tendsto_order.1 A).2 _ B).and self_mem_nhdsWithin).exists

Premises used: StieltjesFunction.toFun
-- 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'
⊢ Nonempty R

Tactic:
have : Nonempty R := ⟨a⟩
-- 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 : ℕ
⊢ f.length (s i) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
have hl :=
      ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')
-- 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∞)
lhs : f.length (s i)
| f.length (s i) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)

Tactic:
lhs
-- 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)

Tactic:
rw [length_eq]

Premises used: StieltjesFunction.length_eq