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
a b : R
this : Nonempty R
a' b' : R
ab : a < b
h : Ioc a b ⊆ Ioc a' b'
h₁ : b ≤ b'
⊢ a' ≤ a

Tactic:
obtain ⟨h₁, h₂⟩ := (Ioc_subset_Ioc_iff ab).1 h

Premises used: Set.Ioc_subset_Ioc_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
ab : a < b
h : Ioc a b ⊆ Ioc a' b'
h₁ : b ≤ b'
h₂ : a' ≤ a
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal

Tactic:
Real.toNNReal_le_toNNReal (sub_le_sub (f.mono h₁) (f.mono h₂))

Premises used: StieltjesFunction.mono, Real.toNNReal_le_toNNReal, sub_le_sub
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
ab : a < b
h : Ioc a b ⊆ Ioc a' b'
h₁ : b ≤ b'
h₂ : a' ≤ a
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal

Tactic:
exact Real.toNNReal_le_toNNReal (sub_le_sub (f.mono h₁) (f.mono h₂))

Premises used: StieltjesFunction.mono, Real.toNNReal_le_toNNReal, sub_le_sub
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
s₁ s₂ : Set R
h : s₁ ⊆ s₂
inl : ∀ (hR : IsEmpty R), f.length s₁ ≤ f.length s₂
inr : ∀ (hR : Nonempty R), f.length s₁ ≤ f.length s₂
⊢ f.length s₁ ≤ f.length s₂

Tactic:
rcases isEmpty_or_nonempty R with hR | hR

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
s₁ s₂ : Set R
h : s₁ ⊆ s₂
hR : IsEmpty R
⊢ f.length s₁ ≤ f.length s₂

Tactic:
simp [length_eq_of_isEmpty]

Premises used: StieltjesFunction.length_eq_of_isEmpty
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
s₁ s₂ : Set R
h : s₁ ⊆ s₂
hR : Nonempty R
inr :
  LE.le (α := ℝ≥0∞) (⨅ (a : R), ⨅ (b : R), ⨅ (_ : s₁ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
    (⨅ (a : R), ⨅ (b : R), ⨅ (_ : s₂ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
⊢ f.length s₁ ≤ f.length s₂

Tactic:
simp only [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
s₁ s₂ : Set R
h : s₁ ⊆ s₂
hR : Nonempty R
⊢ LE.le (α := ℝ≥0∞) (⨅ (a : R), ⨅ (b : R), ⨅ (_ : s₁ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
    (⨅ (a : R), ⨅ (b : R), ⨅ (_ : s₂ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))

Tactic:
iInf_mono fun a => biInf_mono fun b h' => (diff_subset_diff_left h).trans h'

Premises used: HasSubset.Subset.trans, Set.diff_subset_diff_left, iInf_mono, biInf_mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
s₁ s₂ : Set R
h : s₁ ⊆ s₂
hR : Nonempty R
⊢ LE.le (α := ℝ≥0∞) (⨅ (a : R), ⨅ (b : R), ⨅ (_ : s₁ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
    (⨅ (a : R), ⨅ (b : R), ⨅ (_ : s₂ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))

Tactic:
exact iInf_mono fun a => biInf_mono fun b h' => (diff_subset_diff_left h).trans h'

Premises used: HasSubset.Subset.trans, Set.diff_subset_diff_left, iInf_mono, biInf_mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
s : Set R
inl : ∀ (hR : IsEmpty R), f.length (s \ botSet) = f.length s
inr : ∀ (hR : Nonempty R), f.length (s \ botSet) = f.length s
⊢ f.length (s \ botSet) = f.length s

Tactic:
rcases isEmpty_or_nonempty R with hR | hR

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
s : Set R
hR : IsEmpty R
⊢ f.length (s \ botSet) = f.length s

Tactic:
simp [length_eq_of_isEmpty]

Premises used: StieltjesFunction.length_eq_of_isEmpty
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
s : Set R
hR : Nonempty R
⊢ f.length (s \ botSet) = f.length s

Tactic:
simp [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
s : Set R
⊢ (f.outer : (a : Set R) → ℝ≥0∞) s ≤ f.length s

Tactic:
OuterMeasure.ofFunction_le _

Premises used: MeasureTheory.OuterMeasure.ofFunction_le
-- 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 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))
⊢ Icc a b ⊆ ⋃ (i : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) univ i), Iotop (c i) (d i)

Tactic:
simpa using ss
-- 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 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))
rcases :
  ∀ s ⊆ univ,
    ∀ (hf : s.Finite) (hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)),
      ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))

Tactic:
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⟩

Premises used: CompactIccSpace.isCompact_Icc, IsCompact.elim_finite_subcover_image, isOpen_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
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)
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ i ∈ (↑(hf.toFinset (s := s)) : Set ℕ), Iotop (c i) (d i)) (⋃ i ∈ s, Iotop (c i) (d i))

Tactic:
simp only [Finset.set_biUnion_coe,
        Finite.mem_toFinset]

Premises used: Finset.set_biUnion_coe, Set.Finite.mem_toFinset
-- 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 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)
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ i ∈ (↑(hf.toFinset (s := s)) : Set ℕ), Iotop (c i) (d i)) (⋃ i ∈ s, Iotop (c i) (d i))

Tactic:
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]
-- 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 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))
rw :
  ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ⨆ (s : Finset ℕ), ∑ a ∈ s, ofReal ((↑f : R → ℝ) (d a) - (↑f : R → ℝ) (c a))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))

Tactic:
rw [ENNReal.tsum_eq_iSup_sum]

Premises used: ENNReal.tsum_eq_iSup_sum
-- 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 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))

Tactic:
le_trans ?_ (le_iSup _ hf.toFinset)

Premises used: le_iSup, Set.Finite.toFinset, 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 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))
refine :
  ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤
    ∑ a ∈ hf.toFinset (s := s), ofReal ((↑f : R → ℝ) (d a) - (↑f : R → ℝ) (c a))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ⨆ (s : Finset ℕ), ∑ a ∈ s, ofReal ((↑f : R → ℝ) (d a) - (↑f : R → ℝ) (c a))

Tactic:
refine le_trans ?_ (le_iSup _ hf.toFinset)

Premises used: le_iSup, Set.Finite.toFinset, 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 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))
⊢ Icc a b ⊆ ⋃ i ∈ (↑(hf.toFinset (s := s)) : Set ℕ), Iotop (c i) (d i)

Tactic:
simpa only [e]
-- 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 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) ≤
    ∑ a ∈ hf.toFinset (s := s), ofReal ((↑f : R → ℝ) (d a) - (↑f : R → ℝ) (c a))

Tactic:
exact this hf.toFinset _ (by simpa only [e])

Premises used: Set.Finite.toFinset
-- 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 b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ (i : ℕ), Iotop (c i) (d i)
Finset :
  ∀ (s : _root_.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))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), 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])
-- 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 : 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:
fun s => Finset.strongInductionOn s fun s IH b cv => ?_

Premises used: Finset.strongInductionOn
-- 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
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))
⊢ ∀ (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:
refine fun s => Finset.strongInductionOn s fun s IH b cv => ?_
-- 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
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))
inr :
  ∀ (ab : a ≤ b), 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))

Tactic:
rcases le_total b a with ab | ab

Premises used: le_total
-- 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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
ab : b ≤ a
inl : LE.le (α := ℝ≥0∞) 0 (∑ 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))

Tactic:
rw [ENNReal.ofReal_eq_zero.2 (sub_nonpos.2 (f.mono ab))]

Premises used: Iff.mpr, ENNReal.ofReal_eq_zero, StieltjesFunction.mono, sub_nonpos
-- 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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
ab : b ≤ a
⊢ LE.le (α := ℝ≥0∞) 0 (∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i)))

Tactic:
zero_le

Premises used: zero_le
-- 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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
ab : b ≤ a
⊢ LE.le (α := ℝ≥0∞) 0 (∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i)))

Tactic:
exact zero_le

Premises used: zero_le
-- 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
cv : Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i)
ab : a ≤ b
⊢ ∃ i ∈ s, b ∈ Iotop (c i) (d i)

Tactic:
simpa only [SetLike.mem_coe, mem_iUnion, exists_prop] using cv ⟨ab, le_rfl⟩

Premises used: le_rfl, Set.mem_iUnion, exists_prop, SetLike.mem_coe, 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
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
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))
⊢ 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⟩
-- 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
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)
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))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))

Tactic:
rw [← Finset.insert_erase is] at cv ⊢

Premises used: Finset.insert_erase
-- 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 ⊆ ⋃ 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)
⊢ 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

Premises used: Set.biUnion_insert, Finset.coe_insert
-- 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 ⊆ ⋃ 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)
cv₁ : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
⊢ i ∈ s

Tactic:
rw [Finset.coe_insert, biUnion_insert] at cv

Premises used: Set.biUnion_insert, Finset.coe_insert
-- 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 ⊆ ⋃ 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)
cv₁ : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ (↑(s.erase i) : Set ℕ), Iotop (c x) (d x)
is₁ : i ∈ s
⊢ b ∈ Iotop (c i) (d i)

Tactic:
rw [Finset.coe_insert, biUnion_insert] at cv

Premises used: Set.biUnion_insert, Finset.coe_insert
-- 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)
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))
⊢ 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.sum_insert (Finset.notMem_erase _ _)]

Premises used: Finset.notMem_erase, Finset.sum_insert