awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : OrderTopology R
inst_3 : CompactIccSpace R
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a ≤ b
A : Disjoint {a} (Ioc a b)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

Tactic:
simp [← Icc_union_Ioc_eq_Icc le_rfl hab, -singleton_union, ← ENNReal.ofReal_add,
      f.mono.leftLim_le, measure_union A measurableSet_Ioc, f.mono hab]

Premises used: le_rfl, Set.singleton_union, StieltjesFunction.mono, Set.Icc_union_Ioc_eq_Icc, ENNReal.ofReal_add, MeasureTheory.measure_union, Monotone.leftLim_le, measurableSet_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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b < a
inr : 0 = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

Tactic:
simp only [hab, measure_empty, Icc_eq_empty, not_le]

Premises used: not_le, Set.Icc_eq_empty, MeasureTheory.measure_empty
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b < a
inr : ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) = 0
⊢ 0 = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

Tactic:
symm
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b < a
⊢ ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) = 0

Tactic:
simp [ENNReal.ofReal_eq_zero, f.mono.le_leftLim hab]

Premises used: ENNReal.ofReal_eq_zero, StieltjesFunction.mono, Monotone.le_leftLim
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
inl :
  ∀ (hab : b ≤ a),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
inr :
  ∀ (hab : a < b),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)

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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
inl : 0 = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
simp only [hab, measure_empty, Ioo_eq_empty, not_lt]

Premises used: MeasureTheory.measure_empty, not_lt, Set.Ioo_eq_empty
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
inl : ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a) = 0
⊢ 0 = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
symm
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
⊢ ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a) = 0

Tactic:
simp [ENNReal.ofReal_eq_zero, f.mono.leftLim_le hab]

Premises used: ENNReal.ofReal_eq_zero, StieltjesFunction.mono, Monotone.leftLim_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
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
⊢ Disjoint (Ioo a b) {b}

Tactic:
simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
⊢ Disjoint (Ioo a b) {b}

Tactic:
have A : Disjoint (Ioo a b) {b} := by simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ (↑f : R → ℝ) b - (↑f : R → ℝ) a = (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
abel
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
⊢ (↑f : R → ℝ) b - (↑f : R → ℝ) a = (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
have D : f b - f a = f b - leftLim f b + (leftLim f b - f a) := by abel
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
D :
  (↑f : R → ℝ) b - (↑f : R → ℝ) a = (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
have := f.measure_Ioc a b
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
D :
  (↑f : R → ℝ) b - (↑f : R → ℝ) a = (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
this : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ HAdd.hAdd (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
      (ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b)) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
simp only [← Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton,
      measure_union A (measurableSet_singleton b), Icc_self] at this

Premises used: Set.Icc_self, le_rfl, MeasurableSingletonClass.measurableSet_singleton, StieltjesFunction.measure_singleton, Set.Ioo_union_Icc_eq_Ioc, MeasureTheory.measure_union
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
D :
  (↑f : R → ℝ) b - (↑f : R → ℝ) a = (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
this :
  HAdd.hAdd (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
      (ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b)) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
inr :
  ∀
    (this :
      HAdd.hAdd (β := ℝ≥0∞) (ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b))
          (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞) =
        ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b) + ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
inr₁ :
  ∀
    (this :
      HAdd.hAdd (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
          (ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b)) =
        ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a))),
    0 ≤ (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b
inr₂ :
  ∀
    (this :
      HAdd.hAdd (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
          (ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b)) =
        ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a))),
    0 ≤ leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
rw [D, ENNReal.ofReal_add, add_comm] at this

Premises used: add_comm, ENNReal.ofReal_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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
D :
  (↑f : R → ℝ) b - (↑f : R → ℝ) a = (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
this :
  HAdd.hAdd (β := ℝ≥0∞) (ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b))
      (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞) =
    ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b) + ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
simpa only [ENNReal.add_right_inj ENNReal.ofReal_ne_top]

Premises used: ENNReal.add_right_inj, ENNReal.ofReal_ne_top
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
D :
  (↑f : R → ℝ) b - (↑f : R → ℝ) a = (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
this :
  HAdd.hAdd (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
      (ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b)) =
    ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a))
⊢ 0 ≤ (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b

Tactic:
simp only [f.mono.leftLim_le le_rfl, sub_nonneg]

Premises used: le_rfl, StieltjesFunction.mono, Monotone.leftLim_le, sub_nonneg
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint (Ioo a b) {b}
D :
  (↑f : R → ℝ) b - (↑f : R → ℝ) a = (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
this :
  HAdd.hAdd (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞)
      (ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b)) =
    ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) b + (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a))
⊢ 0 ≤ leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a

Tactic:
simp only [f.mono.le_leftLim hab, sub_nonneg]

Premises used: StieltjesFunction.mono, Monotone.le_leftLim, sub_nonneg
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
inl :
  ∀ (hab : b ≤ a),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
inr :
  ∀ (hab : a < b),
    ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
inl : 0 = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

Tactic:
simp only [hab, measure_empty, Ico_eq_empty, not_lt]

Premises used: MeasureTheory.measure_empty, not_lt, Set.Ico_eq_empty
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
inl : ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) = 0
⊢ 0 = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

Tactic:
symm
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
⊢ ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) = 0

Tactic:
simp [ENNReal.ofReal_eq_zero, f.mono.leftLim hab]

Premises used: Monotone.leftLim, ENNReal.ofReal_eq_zero, 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
⊢ Disjoint {a} (Ioo a b)

Tactic:
simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
⊢ Disjoint {a} (Ioo a b)

Tactic:
have A : Disjoint {a} (Ioo a b) := by simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
A : Disjoint {a} (Ioo a b)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)

Tactic:
simp [← Icc_union_Ioo_eq_Ico le_rfl hab, -singleton_union, f.mono.leftLim_le,
      measure_union A measurableSet_Ioo, f.mono.le_leftLim hab, ← ENNReal.ofReal_add]

Premises used: le_rfl, Set.singleton_union, StieltjesFunction.mono, measurableSet_Ioo, ENNReal.ofReal_add, MeasureTheory.measure_union, Set.Icc_union_Ioo_eq_Ico, Monotone.leftLim_le, Monotone.le_leftLim
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
pos :
  ∀ (hx : ∃ (x : R), IsBot x), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (hx : ∀ (x : R), ¬IsBot x), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
by_cases! hx : ∃ x : R, IsBot x
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hx : ∃ (x : R), IsBot x
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [botSet_eq_singleton_of_isBot hx.choose_spec, leftLim_eq_of_isBot hx.choose_spec]

Premises used: Exists.choose_spec, leftLim_eq_of_isBot, botSet_eq_singleton_of_isBot
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
hx : ∀ (x : R), ¬IsBot x
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [botSet, hx]

Premises used: botSet
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
⊢ Nonempty R

Tactic:
have : Nonempty R := ⟨x⟩
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this : Nonempty R
inl : ∀ (val : OrderBot R), ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
inr : NoBotOrder R → ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)

Tactic:
cases botOrderOrNoBotOrder R

Premises used: botOrderOrNoBotOrder
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this : Nonempty R
val : OrderBot R
⊢ Iic x = Icc ⊥ x

Tactic:
simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this : Nonempty R
val : OrderBot R
⊢ Iic x = Icc ⊥ x

Tactic:
have : Iic x = Icc ⊥ x := by simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this_1 : Nonempty R
val : OrderBot R
this : Iic x = Icc ⊥ x
⊢ Tendsto (↑f : R → ℝ) (pure ⊥) (𝓝 l)

Tactic:
rw [atBot_eq_pure_of_isBot isBot_bot] at hf

Premises used: Filter.atBot_eq_pure_of_isBot, isBot_bot
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this_1 : Nonempty R
val : OrderBot R
this : Iic x = Icc ⊥ x
hf₁ : Tendsto (↑f : R → ℝ) (pure ⊥) (𝓝 l)
⊢ Iic x = Icc ⊥ x

Tactic:
rw [atBot_eq_pure_of_isBot isBot_bot] at hf

Premises used: Filter.atBot_eq_pure_of_isBot, isBot_bot
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
x : R
this_1 : Nonempty R
val : OrderBot R
hf : Tendsto (↑f : R → ℝ) (pure ⊥) (𝓝 l)
this : Iic x = Icc ⊥ x
inl : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc ⊥ x) = ofReal ((↑f : R → ℝ) x - l)
inl₁ : ofReal ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) ⊥) = ofReal ((↑f : R → ℝ) x - l)
inl₂ : ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) ⊥) = ofReal ((↑f : R → ℝ) x - l)
inl₃ inl₄ : ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) ⊥) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) ⊥)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)

Tactic:
rw [this, measure_Icc, leftLim_eq_of_isBot isBot_bot,
      tendsto_nhds_unique hf (tendsto_pure_nhds f ⊥)]

Premises used: StieltjesFunction.toFun, Bot.bot, tendsto_pure_nhds, StieltjesFunction.measure_Icc, isBot_bot, leftLim_eq_of_isBot, tendsto_nhds_unique
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this : Nonempty R
val : NoBotOrder R
⊢ NoMinOrder R

Tactic:
have : NoMinOrder R := NoBotOrder.to_noMinOrder R
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
this_1 : Nonempty R
val : NoBotOrder R
this : NoMinOrder R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)

Tactic:
tendsto_nhds_unique (tendsto_measure_Ioc_atBot _ _) ?_

Premises used: MeasureTheory.tendsto_measure_Ioc_atBot, tendsto_nhds_unique