awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ (i : ℕ), Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i) →
      ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
s : Set ℕ
left : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)
e : Eq.{u_1 + 1} (α := Set R) (⋃ i ∈ (↑(hf.toFinset (s := s)) : Set ℕ), Iotop (c i) (d i)) (⋃ i ∈ s, Iotop (c i) (d i))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ⨆ (s : Finset ℕ), ∑ a ∈ s, ofReal ((↑f : R → ℝ) (d a) - (↑f : R → ℝ) (c a))
have refine : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ a ∈ hf.toFinset (s := s), ofReal ((↑f : R → ℝ) (d a) - (↑f : R → ℝ) (c a))
Tactic: refine le_trans ?_ (le_iSup _ hf.toFinset)
-- 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
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ (i : ℕ), Iotop (c i) (d i)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have Finset : ∀ (s : Finset ℕ) (b : R),
  Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i) →
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
Tactic: suffices
    ∀ (s : Finset ℕ) (b), Icc a b ⊆ (⋃ i ∈ (s : Set ℕ), Iotop (c i) (d i)) →
      (ofReal (f b - f a) : ℝ≥0∞) ≤ ∑ i ∈ s, ofReal (f (d i) - f (c i)) by
    rcases isCompact_Icc.elim_finite_subcover_image
        (fun (i : ℕ) (_ : i ∈ univ) => @isOpen_Iotop _ _ _ _ (c i) (d i)) (by simpa using ss) with
      ⟨s, _, hf, hs⟩
    have e : ⋃ i ∈ (hf.toFinset : Set ℕ), Iotop (c i) (d i) = ⋃ i ∈ s, Iotop (c i) (d i) := by
      simp only [Finset.set_biUnion_coe,
        Finite.mem_toFinset]
    rw [ENNReal.tsum_eq_iSup_sum]
    refine le_trans ?_ (le_iSup _ hf.toFinset)
    exact this hf.toFinset _ (by simpa only [e])
-- 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
a : R
c d : ℕ → R
⊢ ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i) →
      ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have refine : ∀ (s 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) (cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)),
  ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
Tactic: refine fun s => Finset.strongInductionOn s fun s IH b cv => ?_
-- 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
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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have inl : ∀ (ab : b ≤ a), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
Tactic: rcases le_total b a with ab | ab
-- 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
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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
inl :
  ∀ (ab : b ≤ a), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have inr : ∀ (ab : a ≤ b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
Tactic: rcases le_total b a with ab | ab
-- 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
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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
ab : b ≤ a
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have inl : LE.le (α := ℝ≥0∞) 0 (∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i)))
Tactic: rw [ENNReal.ofReal_eq_zero.2 (sub_nonpos.2 (f.mono ab))]
-- 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
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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
ab : a ≤ b
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have inr : ∀ (i : ℕ) (is : i ∈ s) (bcd : b ∈ Iotop (c i) (d i)),
  ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
Tactic: obtain ⟨i, is, bcd⟩ : ∃ i ∈ s, b ∈ Iotop (c i) (d i) := by
    simpa only [SetLike.mem_coe, mem_iUnion, exists_prop] using cv ⟨ab, le_rfl⟩
-- 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
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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
ab : a ≤ b
i : ℕ
is : i ∈ s
bcd : b ∈ Iotop (c i) (d i)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have inr : ∀ (cv : Icc a b ⊆ ⋃ i_1 ∈ (↑(insert i (s.erase i)) : Set ℕ), Iotop (c i_1) (d i_1)) (is : i ∈ s)
  (bcd : b ∈ Iotop (c i) (d i)),
  ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
    ∑ i ∈ insert i (s.erase i), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
Tactic: rw [← Finset.insert_erase is] at cv ⊢
Cleared hypotheses: cv, is, bcd
-- 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
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 ⊆ ⋃ i_1 ∈ (↑(insert i (s.erase i)) : Set ℕ), Iotop (c i_1) (d i_1)
is : i ∈ s
bcd : b ∈ Iotop (c i) (d i)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
    ∑ i ∈ insert i (s.erase i), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have cv₁ : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
Tactic: rw [Finset.coe_insert, biUnion_insert] at cv
Cleared hypotheses: cv, is, bcd
-- 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
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)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
    ∑ i ∈ insert i (s.erase i), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have inr : 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: rw [Finset.sum_insert (Finset.notMem_erase _ _)]
-- 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
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)
⊢ 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))
have bcd₁ : b ∈ Ioc (c i) (d i)
Tactic: replace bcd : b ∈ Ioc (c i) (d i) := Iotop_subset_Ioc bcd
Cleared hypotheses: bcd
-- 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
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)
⊢ 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))
have inr : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
  ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i) + ((↑f : R → ℝ) (c i) - (↑f : R → ℝ) a))
Tactic: grw [← IH _ (Finset.erase_ssubset is) (c i), ← ENNReal.ofReal_add_le]
-- 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
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))
⊢ 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))
have inr₁ : Icc a (c i) ⊆ ⋃ i_1 ∈ (↑(s.erase i) : Set ℕ), Iotop (c i_1) (d i_1)
Tactic: grw [← IH _ (Finset.erase_ssubset is) (c i), ← ENNReal.ofReal_add_le]
-- 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
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)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
    ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i) + ((↑f : R → ℝ) (c i) - (↑f : R → ℝ) a))
have inr : (↑f : R → ℝ) b - (↑f : R → ℝ) a ≤ (↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i) + ((↑f : R → ℝ) (c i) - (↑f : R → ℝ) a)
Tactic: gcongr
-- 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
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 → ℝ) (c i) + ((↑f : R → ℝ) (c i) - (↑f : R → ℝ) a)
have inr : (↑f : R → ℝ) b - (↑f : R → ℝ) a ≤ (↑f : R → ℝ) (d i) - (↑f : R → ℝ) a
Tactic: rw [sub_add_sub_cancel]
-- 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
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
⊢ Membership.mem (γ := Set R) (⋃ i_1 ∈ (↑(s.erase i) : Set ℕ), Iotop (c i_1) (d i_1)) x
have apply : ∀ (h : x ∈ Iotop (c i) (d i)), False
Tactic: apply (cv ⟨h₁, le_trans h₂ (le_of_lt bcd.1)⟩).resolve_left (fun h ↦ ?_)
-- 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
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)
⊢ False
have order : ¬False → False
Tactic: order [(Iotop_subset_Ioc h).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
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
⊢ False
have order₄ : True → False
Tactic: order [(Iotop_subset_Ioc h).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
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have refine_1 : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
Tactic: refine le_antisymm ?_ ?_
-- 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
refine_1 : (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) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have refine_2 : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)
Tactic: refine le_antisymm ?_ ?_
-- 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
⊢ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) ≤ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have refine_1 : (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b) ≤ f.length (Ioc a b)
Tactic: rw [← f.length_Ioc]
-- 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
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)
have refine_2 : ∀ (hab : b ≤ a), 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
-- 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
refine_2 : ∀ (hab : b ≤ a), 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)
have refine_2₁ : ∀ (hab : 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
-- 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 : b ≤ a
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)
have this : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) = 0
Tactic: have : ofReal (f b - f a) = 0 := by simpa using f.mono 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
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ (f.outer : (a : Set R) → ℝ≥0∞) (Ioc a b)
have 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∞)
Tactic: apply (le_iInf₂ fun s hs => ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_)
-- 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
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have δpos : 0 < (↑δ : ℝ≥0∞)
Tactic: have δpos : 0 < (δ : ℝ≥0∞) := by simpa [δ] using εpos.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∞)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), f.length (s i) + (↑ε : ℝ≥0∞)
have rcases : ∀ (ε' : ℕ → ℝ≥0) (ε'0 : ∀ (i : ℕ), 0 < ε' i) (hε : ∑' (i : ℕ), (↑(ε' i) : ℝ≥0∞) < (↑δ : ℝ≥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ε⟩
-- 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∞)
⊢ ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a
have refine : ContinuousWithinAt (↑f : R → ℝ) (Ioi a) a
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), (↑f : R → ℝ) a' - (↑f : R → ℝ) a < (↑δ : ℝ) ∧ a < a'
have A : 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
-- 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 : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a
⊢ (↑f : R → ℝ) a - (↑f : R → ℝ) a < (↑δ : ℝ)
have rwa : 0 < (↑δ : ℝ)
Tactic: rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]
-- 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 : ContinuousWithinAt (Y := ℝ) (fun (r : R) ↦ (↑f : R → ℝ) r - (↑f : R → ℝ) a) (Ioi a) a
rwa : 0 < (↑δ : ℝ)
⊢ (↑f : R → ℝ) a - (↑f : R → ℝ) a < (↑δ : ℝ)
have rwa₁ : 0 < δ
Tactic: rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]