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_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
obtain : ∀ (l u : ℝ) (hlu : rightLim f x ∈ Ioo l u) (lus : Ioo l u ⊆ s), ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s

Tactic:
obtain ⟨l, u, hlu, lus⟩ : ∃ l u : ℝ, rightLim f x ∈ Ioo l u ∧ Ioo l u ⊆ s :=
      mem_nhds_iff_exists_Ioo_subset.1 hs

Premises used: Function.rightLim, Iff.mp, mem_nhds_iff_exists_Ioo_subset
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
pos : ∀ (hx : ∀ (y : R), y ≤ x), ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
neg : ∀ (hx : ∃ (y : R), x < y), ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s

Tactic:
by_cases! hx : ∀ y, y ≤ x
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
h : ∀ (hy : x ≤ y), rightLim f y ∈ s
⊢ y ∈ Ici x → rightLim f y ∈ s

Tactic:
(hy : x ≤ y)
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
h : ∀ (y : R) (hy : x ≤ y), rightLim f y ∈ s
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with y (hy : x ≤ y)

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
hy : x ≤ y
⊢ y = x

Tactic:
le_antisymm (hx y) hy

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
hy : x ≤ y
⊢ y = x

Tactic:
exact le_antisymm (hx y) hy

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
hy : x ≤ y
h : rightLim f x ∈ s
⊢ rightLim f y ∈ s

Tactic:
rw [show y = x by exact le_antisymm (hx y) hy]
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
hy : x ≤ y
⊢ rightLim f x ∈ s

Tactic:
lus hlu
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
hy : x ≤ y
⊢ rightLim f x ∈ s

Tactic:
exact lus hlu
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∃ (y : R), x < y
neg : ∀ (y₀ : R) (hy₀ : x < y₀), ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s

Tactic:
rcases hx with ⟨y₀, hy₀⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
⊢ ∃ (y : R), x < y ∧ Ioo x y ⊆ f ⁻¹' Ioo l u

Tactic:
(mem_nhdsGT_iff_exists_Ioo_subset' hy₀).1 (hf.tendsto_rightLim x (Ioo_mem_nhds hlu.1 hlu.2))

Premises used: Set.Ioi, Set.Mem, setOf, mem_nhdsGT_iff_exists_Ioo_subset', Ioo_mem_nhds, And.right, And.left, Monotone.tendsto_rightLim, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
neg : ∀ (y : R) (xy : x < y) (h'y : Ioo x y ⊆ f ⁻¹' Ioo l u), ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s

Tactic:
obtain ⟨y, xy, h'y⟩ : ∃ (y : R), x < y ∧ Ioo x y ⊆ f ⁻¹' Ioo l u :=
      (mem_nhdsGT_iff_exists_Ioo_subset' hy₀).1 (hf.tendsto_rightLim x (Ioo_mem_nhds hlu.1 hlu.2))

Premises used: mem_nhdsGT_iff_exists_Ioo_subset', Ioo_mem_nhds, And.right, And.left, Monotone.tendsto_rightLim, Iff.mp, Set.Ioo
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
h : ∀ (z : R) (hz : z ∈ Ico x y), rightLim f z ∈ s
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s

Tactic:
filter_upwards [Ico_mem_nhdsGE xy] with z hz

Premises used: Ico_mem_nhdsGE
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h : rightLim f z ∈ Ioo l u
⊢ rightLim f z ∈ s

Tactic:
apply lus
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
⊢ rightLim f z ∈ Ioo l u

Tactic:
⟨hlu.1.trans_le (hf.rightLim hz.1), ?_⟩

Premises used: Set.Mem, setOf, And.left, LT.lt.trans_le, And.intro, Monotone.rightLim, Set.Ioo
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h : rightLim f z < u
⊢ rightLim f z ∈ Ioo l u

Tactic:
refine ⟨hlu.1.trans_le (hf.rightLim hz.1), ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h : ∀ (hz : x ∈ Ico x y), rightLim f x < u
h₁ : ∀ (h''z : x < z), rightLim f z < u
⊢ rightLim f z < u

Tactic:
rcases hz.1.eq_or_lt with rfl | h''z

Premises used: LE.le.eq_or_lt, And.left, rfl
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
hz : x ∈ Ico x y
⊢ rightLim f x < u

Tactic:
hlu.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
hz : x ∈ Ico x y
⊢ rightLim f x < u

Tactic:
exact hlu.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h : ∀ (h'z : 𝓝[>] z = ⊥), rightLim f z < u
h₁ : ∀ (h'z : (𝓝[>] z).NeBot), rightLim f z < u
⊢ rightLim f z < u

Tactic:
rcases Filter.eq_or_neBot (𝓝[>] z) with h'z | h'z

Premises used: Set.Ioi, nhdsWithin, Filter.eq_or_neBot
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : 𝓝[>] z = ⊥
h : f z < u
⊢ rightLim f z < u

Tactic:
rw [rightLim_eq_of_eq_bot _ h'z]

Premises used: rightLim_eq_of_eq_bot
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : 𝓝[>] z = ⊥
⊢ z ∈ Ioo x y

Tactic:
have : z ∈ Ioo x y := ⟨h''z, hz.2⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : 𝓝[>] z = ⊥
this : z ∈ Ioo x y
⊢ f z < u

Tactic:
(h'y this).2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : 𝓝[>] z = ⊥
this : z ∈ Ioo x y
⊢ f z < u

Tactic:
exact (h'y this).2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : (𝓝[>] z).NeBot
⊢ ∃ (a : R), z < a ∧ a < y

Tactic:
Filter.nonempty_of_mem (Ioo_mem_nhdsGT hz.2)

Premises used: Set.Mem, Filter.nonempty_of_mem, Set.Nonempty, And.right, Ioo_mem_nhdsGT
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : (𝓝[>] z).NeBot
h : ∀ (a : R) (za : z < a) (ay : a < y), rightLim f z < u
⊢ rightLim f z < u

Tactic:
obtain ⟨a, za, ay⟩ : ∃ a : R, z < a ∧ a < y := Filter.nonempty_of_mem (Ioo_mem_nhdsGT hz.2)

Premises used: Filter.nonempty_of_mem, And.right, Ioo_mem_nhdsGT
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : (𝓝[>] z).NeBot
a : R
za : z < a
ay : a < y
⊢ rightLim f z ≤ f a

Tactic:
hf.rightLim_le za

Premises used: Monotone.rightLim_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : (𝓝[>] z).NeBot
a : R
za : z < a
ay : a < y
⊢ f a < u

Tactic:
(h'y ⟨hz.1.trans_lt za, ay⟩).2

Premises used: And.right, And.left, And.intro, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f_1 : StieltjesFunction R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : (𝓝[>] z).NeBot
a : R
za : z < a
ay : a < y
⊢ rightLim f z < u

Tactic:
calc
        rightLim f z ≤ f a := hf.rightLim_le za
        _ < u := (h'y ⟨hz.1.trans_lt za, ay⟩).2

Premises used: Monotone.rightLim_le, And.right, Function.rightLim, And.left, And.intro, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
⊢ (↑hf.stieltjesFunction : R → ℝ) x = rightLim f x

Tactic:
rfl

Premises used: Function.rightLim, Function.leftLim, rfl, ite
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
f : StieltjesFunction R
⊢ Set.Countable.{u_1} (α := R) {x : R | leftLim (↑f : R → ℝ) x ≠ (↑f : R → ℝ) x}

Tactic:
Countable.mono ?_ f.mono.countable_not_continuousAt

Premises used: Monotone.countable_not_continuousAt, StieltjesFunction.mono, Set.Countable.mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
f : StieltjesFunction R
refine :
  Subset.{u_1} (α := Set R) {x : R | leftLim (↑f : R → ℝ) x ≠ (↑f : R → ℝ) x} {x : R | ¬ContinuousAt (↑f : R → ℝ) x}
⊢ Set.Countable.{u_1} (α := R) {x : R | leftLim (↑f : R → ℝ) x ≠ (↑f : R → ℝ) x}

Tactic:
refine Countable.mono ?_ f.mono.countable_not_continuousAt

Premises used: Monotone.countable_not_continuousAt, StieltjesFunction.mono, Set.Countable.mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
f : StieltjesFunction R
x : R
hx : Membership.mem (γ := Set R) {x : R | leftLim (↑f : R → ℝ) x ≠ (↑f : R → ℝ) x} x
h'x : ContinuousAt (↑f : R → ℝ) x
apply : leftLim (↑f : R → ℝ) x = (↑f : R → ℝ) x
⊢ False

Tactic:
apply hx
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
f : StieltjesFunction R
x : R
hx : Membership.mem (γ := Set R) {x : R | leftLim (↑f : R → ℝ) x ≠ (↑f : R → ℝ) x} x
h'x : ContinuousAt (↑f : R → ℝ) x
⊢ leftLim (↑f : R → ℝ) x = (↑f : R → ℝ) x

Tactic:
(Monotone.continuousWithinAt_Iio_iff_leftLim_eq f.mono).1 h'x.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, Monotone.continuousWithinAt_Iio_iff_leftLim_eq, StieltjesFunction.mono, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
f : StieltjesFunction R
x : R
hx : Membership.mem (γ := Set R) {x : R | leftLim (↑f : R → ℝ) x ≠ (↑f : R → ℝ) x} x
h'x : ContinuousAt (↑f : R → ℝ) x
⊢ leftLim (↑f : R → ℝ) x = (↑f : R → ℝ) x

Tactic:
exact (Monotone.continuousWithinAt_Iio_iff_leftLim_eq f.mono).1 h'x.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, Monotone.continuousWithinAt_Iio_iff_leftLim_eq, StieltjesFunction.mono, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : Nonempty R
s : Set R
⊢ f.length s = ⨅ (a : R), ⨅ (b : R), ⨅ (_ : s \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
simp [length]

Premises used: StieltjesFunction.length
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inst_2 : IsEmpty R
s : Set R
⊢ f.length s = 0

Tactic:
simp only [length, if_pos]

Premises used: StieltjesFunction.length, if_pos
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
inl : ∀ (hR : IsEmpty R), f.length ∅ = 0
inr : ∀ (hR : Nonempty R), f.length ∅ = 0
⊢ f.length ∅ = 0

Tactic:
rcases isEmpty_or_nonempty R with hR | hR

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
hR : IsEmpty R
⊢ f.length ∅ = 0

Tactic:
simp [length_eq_of_isEmpty]

Premises used: StieltjesFunction.length_eq_of_isEmpty
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
hR : Nonempty R
inr : ∀ (inhabited_h : Inhabited R), f.length ∅ = 0
⊢ f.length ∅ = 0

Tactic:
inhabit R
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
hR : Nonempty R
inhabited_h : Inhabited R
inr : Eq (α := ℝ≥0∞) (⨅ (a : R), ⨅ (b : R), ⨅ (_ : ∅ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)) 0
⊢ f.length ∅ = 0

Tactic:
rw [length_eq]

Premises used: StieltjesFunction.length_eq
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
hR : Nonempty R
inhabited_h : Inhabited R
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (_ : Subset.{u_1} (α := Set R) (∅ \ botSet) (Ioc default default)),
      ofReal ((↑f : R → ℝ) default - (↑f : R → ℝ) default))
    0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
hR : Nonempty R
inhabited_h : Inhabited R
⊢ Eq (α := ℝ≥0∞) (⨅ (a : R), ⨅ (b : R), ⨅ (_ : ∅ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)) 0

Tactic:
exact nonpos_iff_eq_zero.1 <| iInf_le_of_le default <| iInf_le_of_le default <| by simp

Premises used: Inhabited.default, Iff.mp, iInf_le_of_le, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
⊢ Nonempty R

Tactic:
have : Nonempty R := ⟨a⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
rw :
  ⨅ (a_1 : R), ⨅ (b_1 : R), ⨅ (_ : Ioc a b \ botSet ⊆ Ioc a_1 b_1), ofReal ((↑f : R → ℝ) b_1 - (↑f : R → ℝ) a_1) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
⊢ f.length (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
rw [length_eq]

Premises used: StieltjesFunction.length_eq
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
⊢ ⨅ (a_1 : R), ⨅ (b_1 : R), ⨅ (_ : Ioc a b \ botSet ⊆ Ioc a_1 b_1), ofReal ((↑f : R → ℝ) b_1 - (↑f : R → ℝ) a_1) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
le_antisymm (iInf_le_of_le a <| iInf₂_le b diff_subset)
      (le_iInf fun a' => le_iInf fun b' => le_iInf fun h => ENNReal.coe_le_coe.2 ?_)

Premises used: Iff.mpr, iInf₂_le, le_iInf, ENNReal.coe_le_coe, le_antisymm, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
le_antisymm :
  ∀ (a' b' : R) (h : Ioc a b \ botSet ⊆ Ioc a' b'),
    ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
⊢ ⨅ (a_1 : R), ⨅ (b_1 : R), ⨅ (_ : Ioc a b \ botSet ⊆ Ioc a_1 b_1), ofReal ((↑f : R → ℝ) b_1 - (↑f : R → ℝ) a_1) =
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)

Tactic:
refine
    le_antisymm (iInf_le_of_le a <| iInf₂_le b diff_subset)
      (le_iInf fun a' => le_iInf fun b' => le_iInf fun h => ENNReal.coe_le_coe.2 ?_)

Premises used: Iff.mpr, le_iInf, ENNReal.coe_le_coe, le_antisymm, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
inl : ∀ (ab : b ≤ a), ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
inr : ∀ (ab : a < b), ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal

Tactic:
rcases le_or_gt b a with ab | ab

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
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
ab : b ≤ a
inl : 0 ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal

Tactic:
rw [Real.toNNReal_of_nonpos (sub_nonpos.2 (f.mono ab))]

Premises used: Iff.mpr, StieltjesFunction.mono, Real.toNNReal_of_nonpos, sub_nonpos
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
ab : b ≤ a
⊢ 0 ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal

Tactic:
apply zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
ab : a < b
⊢ Ioc a b ⊆ Ioc a' b'

Tactic:
simp only [Ioc_diff_botSet] at h

Premises used: Ioc_diff_botSet
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
ab : a < b
h : Ioc a b ⊆ Ioc a' b'
⊢ b ≤ b'

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

Premises used: Set.Ioc_subset_Ioc_iff, Iff.mp