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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a ≤ b
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have A : Disjoint {a} (Ioc a b)
Tactic: have A : Disjoint {a} (Ioc a b) := by simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b < a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc a b) = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have inr : 0 = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
Tactic: simp only [hab, measure_empty, Icc_eq_empty, not_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
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b < a
⊢ 0 = ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have inr : ofReal ((↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) = 0
Tactic: symm
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have inl : ∀ (hab : b ≤ 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)
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have inr : ∀ (hab : a < b),
  ((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)
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have inl : 0 = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
Tactic: simp only [hab, measure_empty, Ioo_eq_empty, not_lt]
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have inl : ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a) = 0
Tactic: symm
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have A : Disjoint (Ioo a b) {b}
Tactic: have A : Disjoint (Ioo a b) {b} := by simp
-- 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 : 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.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have D : (↑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
-- 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 : 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∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have this : ((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
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: simp only [← Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton,
      measure_union A (measurableSet_singleton b), Icc_self] at this
Cleared hypotheses: this
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: rw [D, ENNReal.ofReal_add, add_comm] at this
Cleared hypotheses: this
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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
Tactic: rw [D, ENNReal.ofReal_add, add_comm] at this
Cleared hypotheses: this
-- 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 : 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
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioo a b) = ofReal (leftLim (↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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
Tactic: rw [D, ENNReal.ofReal_add, add_comm] at this
Cleared hypotheses: this
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have inl : ∀ (hab : b ≤ 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)
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have inr : ∀ (hab : a < b),
  ((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)
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have inl : 0 = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
Tactic: simp only [hab, measure_empty, Ico_eq_empty, not_lt]
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have inl : ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a) = 0
Tactic: symm
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
a b : R
hab : a < b
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ico a b) = ofReal (leftLim (↑f : R → ℝ) b - leftLim (↑f : R → ℝ) a)
have A : Disjoint {a} (Ioo a b)
Tactic: have A : Disjoint {a} (Ioo a b) := by simp
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : ∀ (hx : ∃ (x : R), IsBot x), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: by_cases! hx : ∃ x : R, IsBot x
-- 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 : 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∞)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)
have neg : ∀ (hx : ∀ (x : R), ¬IsBot x), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) botSet : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: by_cases! hx : ∃ x : R, IsBot x
-- 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
x : R
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have this : Nonempty R
Tactic: have : Nonempty R := ⟨x⟩
-- 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 : 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
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have inl : ∀ (val : OrderBot R), ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
Tactic: cases botOrderOrNoBotOrder R
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have inr : NoBotOrder R → ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
Tactic: cases botOrderOrNoBotOrder R
-- 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 : 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
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have this₁ : Iic x = Icc ⊥ x
Tactic: have : Iic x = Icc ⊥ x := by simp
-- 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 : 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
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have hf₁ : Tendsto (↑f : R → ℝ) (pure ⊥) (𝓝 l)
Tactic: rw [atBot_eq_pure_of_isBot isBot_bot] at hf
Cleared hypotheses: hf, this
-- 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 : 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
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have inl : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc ⊥ 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 ⊥)]
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have inl₁ : ofReal ((↑f : R → ℝ) x - leftLim (↑f : R → ℝ) ⊥) = ofReal ((↑f : R → ℝ) x - l)
Tactic: rw [this, measure_Icc, leftLim_eq_of_isBot isBot_bot,
      tendsto_nhds_unique hf (tendsto_pure_nhds f ⊥)]
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have inl₂ : ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) ⊥) = ofReal ((↑f : R → ℝ) x - l)
Tactic: rw [this, measure_Icc, leftLim_eq_of_isBot isBot_bot,
      tendsto_nhds_unique hf (tendsto_pure_nhds f ⊥)]
-- 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 : 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)
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have inl₃ : ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) ⊥) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) ⊥)
Tactic: rw [this, measure_Icc, leftLim_eq_of_isBot isBot_bot,
      tendsto_nhds_unique hf (tendsto_pure_nhds f ⊥)]
-- 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 : 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
⊢ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
have this₁ : NoMinOrder R
Tactic: have : NoMinOrder R := NoBotOrder.to_noMinOrder R
-- 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 : 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)
have inr : Tendsto (fun (x_1 : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc x_1 x)) atBot
  (𝓝 (ofReal ((↑f : R → ℝ) x - l)))
Tactic: refine tendsto_nhds_unique (tendsto_measure_Ioc_atBot _ _) ?_