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
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
x : R
hx : (↑f : R → ℝ) x ≤ -C - 1
⊢ ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)

Tactic:
grind
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
H : ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
⊢ ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)

Tactic:
H
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
H : ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)
⊢ ∃ (l : ℝ), Tendsto (↑f : R → ℝ) atBot (𝓝 l)

Tactic:
exact H
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
inr : ∀ (l : ℝ) (hl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)), IsFiniteMeasure (m0 := inst_4) f.measure
⊢ 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
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
l : ℝ
hl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
⊢ IsFiniteMeasure (m0 := inst_4) f.measure

Tactic:
f.isFiniteMeasure hl hu

Premises used: StieltjesFunction.isFiniteMeasure
-- 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
C : ℝ
h : ∀ (x : R), |(↑f : R → ℝ) x| ≤ C
h_1 : Nonempty R
u : ℝ
hu : Tendsto (↑f : R → ℝ) atTop (𝓝 u)
l : ℝ
hl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
⊢ IsFiniteMeasure (m0 := inst_4) f.measure

Tactic:
exact f.isFiniteMeasure hl hu

Premises used: StieltjesFunction.isFiniteMeasure
-- 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
inst_8 : Nonempty R
hf_bot : Tendsto (↑f : R → ℝ) atBot (𝓝 0)
hf_top : Tendsto (↑f : R → ℝ) atTop (𝓝 1)
⊢ Eq (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [f.measure_univ hf_bot hf_top]

Premises used: StieltjesFunction.measure_univ
-- 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
⊢ IsLocallyFiniteMeasure (m0 := inst_4) f.measure

Tactic:
⟨fun x ↦ ?_⟩

Premises used: MeasureTheory.IsLocallyFiniteMeasure.mk
-- 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
refine : ∀ (x : R), Measure.FiniteAtFilter (_m0 := inst_4) f.measure (𝓝 x)
⊢ IsLocallyFiniteMeasure (m0 := inst_4) f.measure

Tactic:
refine ⟨fun 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
x : R
⊢ univ ∈ 𝓝 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
x : R
obtain : ∀ (b c : R) (h : Icc b c ∈ 𝓝 x), Measure.FiniteAtFilter (_m0 := inst_4) f.measure (𝓝 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)

Premises used: Set.univ, nhds, exists_Icc_mem_subset_of_mem_nhds
-- 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
x b c : R
h : Icc b c ∈ 𝓝 x
⊢ LT.lt (α := ℝ≥0∞) (((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Icc b c) : ℝ≥0∞) (∞ : ℝ≥0∞)

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
x b c : R
h : Icc b c ∈ 𝓝 x
⊢ Measure.FiniteAtFilter (_m0 := inst_4) f.measure (𝓝 x)

Tactic:
exact ⟨Icc b c, h, 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
g : StieltjesFunction R
l : ℝ
hfg : Eq (α := Measure R) f.measure g.measure
hfl : Tendsto (↑f : R → ℝ) atBot (𝓝 l)
hgl : Tendsto (↑g : R → ℝ) atBot (𝓝 l)
h : ∀ (x : R), (↑f : R → ℝ) x = (↑g : R → ℝ) x
⊢ f = g

Tactic:
ext 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
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.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Iic x) = ofReal ((↑f : R → ℝ) x - l)

Tactic:
have hf := measure_Iic f hfl 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
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
h₂ : ∀ (hf : ofReal ((↑g : R → ℝ) x - l) = ofReal ((↑f : R → ℝ) x - l)), 0 ≤ (↑f : 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

Premises used: ENNReal.ofReal_eq_ofReal_iff, eq_comm, StieltjesFunction.measure_Iic
-- 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
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 : R → ℝ) x - l = (↑g : R → ℝ) x - l
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x

Tactic:
simpa using hf
-- 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
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)
h : l ≤ (↑g : R → ℝ) x
⊢ 0 ≤ (↑g : R → ℝ) x - l

Tactic:
rw [sub_nonneg]

Premises used: 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
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)
⊢ l ≤ (↑g : R → ℝ) x

Tactic:
Monotone.le_of_tendsto g.mono hgl x

Premises used: StieltjesFunction.mono, Monotone.le_of_tendsto
-- 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
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)
⊢ l ≤ (↑g : R → ℝ) x

Tactic:
exact Monotone.le_of_tendsto g.mono hgl x

Premises used: StieltjesFunction.mono, Monotone.le_of_tendsto
-- 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
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)
h : l ≤ (↑f : R → ℝ) x
⊢ 0 ≤ (↑f : R → ℝ) x - l

Tactic:
rw [sub_nonneg]

Premises used: 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
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)
⊢ l ≤ (↑f : R → ℝ) x

Tactic:
Monotone.le_of_tendsto f.mono hfl x

Premises used: StieltjesFunction.mono, Monotone.le_of_tendsto
-- 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
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)
⊢ l ≤ (↑f : R → ℝ) x

Tactic:
exact Monotone.le_of_tendsto f.mono hfl x

Premises used: StieltjesFunction.mono, Monotone.le_of_tendsto
-- 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
g : StieltjesFunction R
y : R
hfg : Eq (α := Measure R) f.measure g.measure
hy : (↑f : R → ℝ) y = (↑g : R → ℝ) y
h : ∀ (x : R), (↑f : R → ℝ) x = (↑g : R → ℝ) x
⊢ f = g

Tactic:
ext 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
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.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
-- 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
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
h₂ :
  ∀ (hf : ofReal ((↑g : R → ℝ) y - (↑g : R → ℝ) x) = ofReal ((↑f : R → ℝ) y - (↑f : R → ℝ) x)),
    0 ≤ (↑f : R → ℝ) y - (↑f : 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

Premises used: ENNReal.ofReal_eq_ofReal_iff, eq_comm, StieltjesFunction.measure_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
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 : (↑g : R → ℝ) y - (↑f : R → ℝ) x = (↑g : R → ℝ) y - (↑g : R → ℝ) x
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x

Tactic:
simpa using hf
-- 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
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)
h : (↑g : R → ℝ) x ≤ (↑g : R → ℝ) y
⊢ 0 ≤ (↑g : R → ℝ) y - (↑g : R → ℝ) x

Tactic:
rw [sub_nonneg]

Premises used: 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
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)
⊢ (↑g : R → ℝ) x ≤ (↑g : R → ℝ) y

Tactic:
g.mono hxy

Premises used: 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
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)
⊢ (↑g : R → ℝ) x ≤ (↑g : R → ℝ) y

Tactic:
exact g.mono hxy

Premises used: 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
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)
h : (↑f : R → ℝ) x ≤ (↑f : R → ℝ) y
⊢ 0 ≤ (↑f : R → ℝ) y - (↑f : R → ℝ) x

Tactic:
rw [sub_nonneg]

Premises used: 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
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)
⊢ (↑f : R → ℝ) x ≤ (↑f : R → ℝ) y

Tactic:
f.mono hxy

Premises used: 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
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)
⊢ (↑f : R → ℝ) x ≤ (↑f : R → ℝ) y

Tactic:
exact f.mono hxy

Premises used: 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
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.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
-- 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
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
hf : ((f.measure : Measure R) : (a : Set R) → ℝ≥0∞) (Ioc y x) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
h : ∀ (hf : (↑f : R → ℝ) x - (↑g : R → ℝ) y = (↑g : R → ℝ) x - (↑g : R → ℝ) y), (↑f : R → ℝ) x = (↑g : R → ℝ) x
h₁ :
  ∀ (hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)),
    0 ≤ (↑g : R → ℝ) x - (↑g : R → ℝ) y
h₂ :
  ∀ (hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)),
    0 ≤ (↑f : R → ℝ) x - (↑f : R → ℝ) y
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x

Tactic:
rw [hfg, measure_Ioc g y x, ENNReal.ofReal_eq_ofReal_iff, eq_comm, hy] at hf

Premises used: ENNReal.ofReal_eq_ofReal_iff, eq_comm, StieltjesFunction.measure_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
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
hf : (↑f : R → ℝ) x - (↑g : R → ℝ) y = (↑g : R → ℝ) x - (↑g : R → ℝ) y
⊢ (↑f : R → ℝ) x = (↑g : R → ℝ) x

Tactic:
simpa using hf
-- 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
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
hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
h : (↑g : R → ℝ) y ≤ (↑g : R → ℝ) x
⊢ 0 ≤ (↑g : R → ℝ) x - (↑g : R → ℝ) y

Tactic:
rw [sub_nonneg]

Premises used: 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
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
hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
⊢ (↑g : R → ℝ) y ≤ (↑g : R → ℝ) x

Tactic:
g.mono hxy

Premises used: 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
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
hf : ofReal ((↑g : R → ℝ) x - (↑g : R → ℝ) y) = ofReal ((↑f : R → ℝ) x - (↑f : R → ℝ) y)
⊢ (↑g : R → ℝ) y ≤ (↑g : R → ℝ) x

Tactic:
exact g.mono hxy

Premises used: StieltjesFunction.mono