awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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
⊢ ∃ (a' : R), (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ) ∧ a < a'
have B : (↑f : R → ℝ) a - (↑f : R → ℝ) a < (↑δ : ℝ)
Tactic: have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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' : R), (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ) ∧ a < a'
have this : (𝓝[>] a).NeBot
Tactic: have : (𝓝[>] a).NeBot := nhdsGT_neBot_of_exists_gt ⟨b, hab⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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'
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have this : Nonempty R
Tactic: have : Nonempty R := ⟨a⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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 : 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∞)
have hl : 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')
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
| f.length (s i) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
have lhs : f.length (s i)
Tactic: lhs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
| f.length (s i)
have rw : ⨅ (a : R), ⨅ (b : R), ⨅ (_ : s i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
Tactic: rw [length_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
| f.length (s i) < f.length (s i) + (↑(ε' i) : ℝ≥0∞)
have rw : ⨅ (a : R), ⨅ (b : R), ⨅ (_ : s i \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
Tactic: lhs
      rw [length_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
⊢ ∃ (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∞)
have hl₁ : ⨅ (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]
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
⊢ ∃ (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∞)
have 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∞)
Tactic: simp only [iInf_lt_iff, exists_prop] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
⊢ ∃ (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∞)
have 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∞)
Tactic: rcases hl with ⟨p, q', spq, hq'⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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 ∈ Ioc p q'
have a₁ : x ∈ s i \ botSet
Tactic: apply spq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
⊢ ∃ (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∞)
have A : 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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'
⊢ ∃ (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∞)
have 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∞)
Tactic: by_cases htq' : IsTop q'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
⊢ ∃ (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∞)
have 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∞)
Tactic: by_cases htq' : IsTop q'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
have pos : Icc a' b ∩ s i ⊆ Iotop (p, q').1 (p, q').2
Tactic: refine ⟨(p, q'), ?_, hq'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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
⊢ x ∈ Iotop (p, q').1 (p, q').2
have pos : p < x ∧ x ≤ q'
Tactic: simp only [Iotop, htq', ↓reduceIte, mem_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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∞)
have this₁ : (𝓝[>] q').NeBot
Tactic: have : (𝓝[>] q').NeBot := by simp [Filter.neBot_iff, nhdsGT_eq_bot_iff, htq', not_covBy]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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'
have apply : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) p) (Ioi q') q'
Tactic: apply ENNReal.continuous_ofReal.continuousAt.comp_continuousWithinAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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'
have refine : ContinuousWithinAt (↑f : R → ℝ) (Ioi q') q'
Tactic: refine ContinuousWithinAt.sub ?_ continuousWithinAt_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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
⊢ ∃ (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∞)
have this₁ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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'
⊢ ∃ (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∞)
have 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∞)
Tactic: rcases (((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : 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
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have this₁ : ∀ (i : ℕ),
  ∃ (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: have : ∀ i, ∃ p : R × R, Icc a' b ∩ s i ⊆ Iotop p.1 p.2 ∧
      (ofReal (f p.2 - f p.1) : ℝ≥0∞) < f.length (s i) + ε' i := by
    intro i
    have hl :=
      ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_ne_zero.2 (ε'0 i).ne')
    conv at hl =>
      lhs
      rw [length_eq]
    simp only [iInf_lt_iff, exists_prop] at hl
    rcases hl with ⟨p, q', spq, hq'⟩
    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)]
    by_cases htq' : IsTop q'
    · refine ⟨(p, q'), ?_, hq'⟩
      rintro x hx
      simp only [Iotop, htq', ↓reduceIte, mem_Ioc]
      exact ⟨(A hx).1, htq' _⟩
    have : (𝓝[>] q').NeBot := by simp [Filter.neBot_iff, nhdsGT_eq_bot_iff, htq', not_covBy]
    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
    rcases (((tendsto_order.1 this).2 _ hq').and self_mem_nhdsWithin).exists with ⟨q, hq, q'q⟩
    exact ⟨⟨p, q⟩, A.trans ((Ioc_subset_Ioo_right q'q).trans Ioo_subset_Iotop), hq⟩