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
inst_4 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
inst_8 : Nonempty R
l u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ Tendsto (fun (x : R) ↦ ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x)) atTop (𝓝 (ofReal (u - l)))
have simp_rw : Tendsto (fun (x : R) ↦ ofReal ((↑f : R → ℝ) x - l)) atTop (𝓝 (ofReal (u - l)))
Tactic: simp_rw [measure_Iic f hfl]
-- 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atTop atTop
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have inhabit : ∀ (inhabited_h : Inhabited R), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: inhabit 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atTop atTop
inhabited_h : Inhabited R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioi default) : ℝ≥0∞)
  (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf default]
-- 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atBot atBot
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have inhabit : ∀ (inhabited_h : Inhabited R), Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: inhabit 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
inst_8 : Nonempty R
hf : Tendsto (↑f : R → ℝ) atBot atBot
inhabited_h : Inhabited R
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iio default) : ℝ≥0∞)
  (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf default]
-- 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 u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ IsFiniteMeasure (m0 := inst_4) f.measure
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- 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 u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have measure_univ_lt_top : IsEmpty R → LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: cases isEmpty_or_nonempty 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 u : ℝ
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hfu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
measure_univ_lt_top :
  IsEmpty R → LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have measure_univ_lt_top₁ : Nonempty R → LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: cases isEmpty_or_nonempty 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
⊢ IsFiniteMeasure (m0 := inst_4) f.measure
have inl : IsEmpty R → IsFiniteMeasure (m0 := inst_4) f.measure
Tactic: cases isEmpty_or_nonempty 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
inl : IsEmpty R → IsFiniteMeasure (m0 := inst_4) f.measure
⊢ IsFiniteMeasure (m0 := inst_4) f.measure
have inr : Nonempty R → IsFiniteMeasure (m0 := inst_4) f.measure
Tactic: cases isEmpty_or_nonempty 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
⊢ ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
have inl : ∀ (H : Tendsto (↑f : R → ℝ) atTop atTop), ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
Tactic: rcases tendsto_atTop_of_monotone f.mono with H | 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
inl : ∀ (H : Tendsto (↑f : R → ℝ) atTop atTop), ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
have inr : ∀ (H : ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 l)), ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
Tactic: rcases tendsto_atTop_of_monotone f.mono with H | 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
H : Tendsto (↑f : R → ℝ) atTop atTop
⊢ ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
have inl : ∀ (x : R) (hx : C + 1 ≤ (↑f : R → ℝ) x), ∃ (u : ℝ), Tendsto (↑f : R → ℝ) atTop (𝓝 u)
Tactic: obtain ⟨x, hx⟩ : ∃ x, C + 1 ≤ f x := (tendsto_atTop.1 H (C + 1)).exists
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
⊢ IsFiniteMeasure (m0 := inst_4) f.measure
have inr : ∀ (u : ℝ) (hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)), IsFiniteMeasure (m0 := inst_4) f.measure
Tactic: obtain ⟨u, hu⟩ : ∃ u, Tendsto f atTop (𝓝 u) := by
    rcases tendsto_atTop_of_monotone f.mono with H | H
    · obtain ⟨x, hx⟩ : ∃ x, C + 1 ≤ f x := (tendsto_atTop.1 H (C + 1)).exists
      grind
    exact 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
have inl : ∀ (H : Tendsto (↑f : R → ℝ) atBot atBot), ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
Tactic: rcases tendsto_atBot_of_monotone f.mono with H | 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
inl : ∀ (H : Tendsto (↑f : R → ℝ) atBot atBot), ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
⊢ ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
have inr : ∀ (H : ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)), ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
Tactic: rcases tendsto_atBot_of_monotone f.mono with H | 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
H : Tendsto (↑f : R → ℝ) atBot atBot
⊢ ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
have inl : ∀ (x : R) (hx : (↑f : R → ℝ) x ≤ -C - 1), ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
Tactic: obtain ⟨x, hx⟩ : ∃ x, f x ≤ - C - 1 := (tendsto_atBot.1 H (-C - 1)).exists
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
⊢ IsFiniteMeasure (m0 := inst_4) f.measure
have inr : ∀ (l : ℝ) (hl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)), IsFiniteMeasure (m0 := inst_4) f.measure
Tactic: obtain ⟨l, hl⟩ : ∃ l, Tendsto f atBot (𝓝 l) := by
    rcases tendsto_atBot_of_monotone f.mono with H | H
    · obtain ⟨x, hx⟩ : ∃ x, f x ≤ - C - 1 := (tendsto_atBot.1 H (-C - 1)).exists
      grind
    exact 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 : MeasurableSpace R
inst_5 : BorelSpace R
inst_6 : SecondCountableTopology R
inst_7 : DenselyOrdered R
⊢ IsLocallyFiniteMeasure (m0 := inst_4) f.measure
have refine : ∀ (x : R), Measure.FiniteAtFilter (_m0 := inst_4) f.measure (𝓝 x)
Tactic: refine ⟨fun 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
x : R
⊢ Measure.FiniteAtFilter (_m0 := inst_4) f.measure (𝓝 x)
have obtain : ∀ (b c : R) (h : Icc b c ∈ 𝓝 x), Measure.FiniteAtFilter (_m0 := inst_4) f.measure (𝓝 x)
Tactic: obtain ⟨b, c, -, h, -⟩ : ∃ b c, x ∈ Icc b c ∧ Icc b c ∈ 𝓝 x ∧ Icc b c ⊆ univ :=
    exists_Icc_mem_subset_of_mem_nhds (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
g : StieltjesFunction R
l : ℝ
hfg : Eq (α := Measure R) f.measure g.measure
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hgl : Tendsto (↑g : R → ℝ) atBot (𝓝 l)
⊢ f = g
have h : ∀ (x : R), (↑f : R → ℝ) x = (↑g : R → ℝ) x
Tactic: ext 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
g : StieltjesFunction R
l : ℝ
hfg : Eq (α := Measure R) f.measure g.measure
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hgl : Tendsto (↑g : R → ℝ) atBot (𝓝 l)
x : R
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
Tactic: have hf := measure_Iic f hfl 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
g : StieltjesFunction R
l : ℝ
hfg : Eq (α := Measure R) f.measure g.measure
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hgl : Tendsto (↑g : R → ℝ) atBot (𝓝 l)
x : R
hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h : ∀ (hf : (↑f : R → ℝ) x - l = (↑g : R → ℝ) x - l), (↑f : R → ℝ) x = (↑g : R → ℝ) x
Tactic: rw [hfg, measure_Iic g hgl x, ENNReal.ofReal_eq_ofReal_iff, eq_comm] at hf
Cleared hypotheses: hf
-- 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
g : StieltjesFunction R
l : ℝ
hfg : Eq (α := Measure R) f.measure g.measure
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hgl : Tendsto (↑g : R → ℝ) atBot (𝓝 l)
x : R
hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
h : ∀ (hf : (↑f : R → ℝ) x - l = (↑g : R → ℝ) x - l), (↑f : R → ℝ) x = (↑g : R → ℝ) x
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h₁ : ∀ (hf : ofReal ((↑g : R → ℝ) x - l) = ofReal ((↑f : R → ℝ) x - l)), 0 ≤ (↑g : R → ℝ) x - l
Tactic: rw [hfg, measure_Iic g hgl x, ENNReal.ofReal_eq_ofReal_iff, eq_comm] at hf
Cleared hypotheses: hf
-- 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
g : StieltjesFunction R
l : ℝ
hfg : Eq (α := Measure R) f.measure g.measure
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hgl : Tendsto (↑g : R → ℝ) atBot (𝓝 l)
x : R
hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)
h : ∀ (hf : (↑f : R → ℝ) x - l = (↑g : R → ℝ) x - l), (↑f : R → ℝ) x = (↑g : R → ℝ) x
h₁ : ∀ (hf : ofReal ((↑g : R → ℝ) x - l) = ofReal ((↑f : R → ℝ) x - l)), 0 ≤ (↑g : R → ℝ) x - l
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h₂ : ∀ (hf : ofReal ((↑g : R → ℝ) x - l) = ofReal ((↑f : R → ℝ) x - l)), 0 ≤ (↑f : R → ℝ) x - l
Tactic: rw [hfg, measure_Iic g hgl x, ENNReal.ofReal_eq_ofReal_iff, eq_comm] at hf
Cleared hypotheses: hf
-- 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
g : StieltjesFunction R
l : ℝ
hfg : Eq (α := Measure R) f.measure g.measure
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hgl : Tendsto (↑g : R → ℝ) atBot (𝓝 l)
x : R
hf : ofReal ((↑g : R → ℝ) x - l) = ofReal ((↑f : R → ℝ) x - l)
⊢ 0 ≤ (↑g : R → ℝ) x - l
have h : l ≤ (↑g : R → ℝ) x
Tactic: rw [sub_nonneg]
-- 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
g : StieltjesFunction R
l : ℝ
hfg : Eq (α := Measure R) f.measure g.measure
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hgl : Tendsto (↑g : R → ℝ) atBot (𝓝 l)
x : R
hf : ofReal ((↑g : R → ℝ) x - l) = ofReal ((↑f : R → ℝ) x - l)
⊢ 0 ≤ (↑f : R → ℝ) x - l
have h : l ≤ (↑f : R → ℝ) x
Tactic: rw [sub_nonneg]
-- 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
⊢ f = g
have h : ∀ (x : R), (↑f : R → ℝ) x = (↑g : R → ℝ) x
Tactic: ext 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : x ≤ y
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc x y) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)
Tactic: have hf := measure_Ioc f x y
-- 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : x ≤ y
hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc x y) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h : ∀ (hf : (↑g : R → ℝ) y - (↑f : R → ℝ) x = (↑g : R → ℝ) y - (↑g : R → ℝ) x), (↑f : R → ℝ) x = (↑g : R → ℝ) x
Tactic: rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
Cleared hypotheses: hf
-- 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : x ≤ y
hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc x y) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)
h : ∀ (hf : (↑g : R → ℝ) y - (↑f : R → ℝ) x = (↑g : R → ℝ) y - (↑g : R → ℝ) x), (↑f : R → ℝ) x = (↑g : R → ℝ) x
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h₁ : ∀ (hf : ofReal ((↑g : R → ℝ) y - (↑g : R → ℝ) x) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)),
  0 ≤ (↑g : R → ℝ) y - (↑g : R → ℝ) x
Tactic: rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
Cleared hypotheses: hf
-- 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : x ≤ y
hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc x y) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)
h : ∀ (hf : (↑g : R → ℝ) y - (↑f : R → ℝ) x = (↑g : R → ℝ) y - (↑g : R → ℝ) x), (↑f : R → ℝ) x = (↑g : R → ℝ) x
h₁ :
  ∀ (hf : ofReal ((↑g : R → ℝ) y - (↑g : R → ℝ) x) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)),
    0 ≤ (↑g : R → ℝ) y - (↑g : R → ℝ) x
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have h₂ : ∀ (hf : ofReal ((↑g : R → ℝ) y - (↑g : R → ℝ) x) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)),
  0 ≤ (↑f : R → ℝ) y - (↑f : R → ℝ) x
Tactic: rw [hfg, measure_Ioc g x y, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf
Cleared hypotheses: hf
-- 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : x ≤ y
hf : ofReal ((↑g : R → ℝ) y - (↑g : R → ℝ) x) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)
⊢ 0 ≤ (↑g : R → ℝ) y - (↑g : R → ℝ) x
have h : (↑g : R → ℝ) x ≤ (↑g : R → ℝ) y
Tactic: rw [sub_nonneg]
-- 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : x ≤ y
hf : ofReal ((↑g : R → ℝ) y - (↑g : R → ℝ) x) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)
⊢ 0 ≤ (↑f : R → ℝ) y - (↑f : R → ℝ) x
have h : (↑f : R → ℝ) x ≤ (↑f : R → ℝ) y
Tactic: rw [sub_nonneg]
-- 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
x : R
hxy : y ≤ x
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x
have hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc y x) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
Tactic: have hf := measure_Ioc f y x