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
inst_2 : OrderTopology R
inst_3 : DenselyOrdered R
inst_4 : NoMaxOrder R
f : StieltjesFunction R
x : R
this : rightLim (↑f : R → ℝ) x = ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R)
⊢ ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R) = (↑f : R → ℝ) x
have rw : rightLim (↑f : R → ℝ) x = (↑f : R → ℝ) x
Tactic: rw [← this, f.rightLim_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : DenselyOrdered R
inst_4 : NoMaxOrder R
f : StieltjesFunction R
x : R
this : rightLim (↑f : R → ℝ) x = ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R)
rw : rightLim (↑f : R → ℝ) x = (↑f : R → ℝ) x
⊢ ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R) = (↑f : R → ℝ) x
have rw₁ : (↑f : R → ℝ) x = (↑f : R → ℝ) x
Tactic: rw [← this, f.rightLim_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : DenselyOrdered R
inst_4 : NoMaxOrder R
f : StieltjesFunction R
x : R
⊢ ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R) = (↑f : R → ℝ) x
have suffices : rightLim (↑f : R → ℝ) x = ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R)
Tactic: suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.rightLim_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : DenselyOrdered R
inst_4 : NoMaxOrder R
f : StieltjesFunction R
x : R
⊢ rightLim (↑f : R → ℝ) x = ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R)
have rw : 𝓝[>] x ≠ ⊥
Tactic: rw [f.mono.rightLim_eq_sInf, sInf_image']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : DenselyOrdered R
inst_4 : NoMaxOrder R
f : StieltjesFunction R
x : R
⊢ 𝓝[>] x ≠ ⊥
have rw : (𝓝[>] x).NeBot
Tactic: rw [← neBot_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
f : StieltjesFunction ℝ
x : ℝ
⊢ ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑f : ℝ → ℝ) (↑(↑r : ℚ) : ℝ) = (↑f : ℝ → ℝ) x
have rw : Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑f : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
  (⨅ (r : (↑(Ioi x) : Type)), (↑f : ℝ → ℝ) (↑r : ℝ))
Tactic: rw [← iInf_Ioi_eq f x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
f : StieltjesFunction ℝ
x : ℝ
⊢ Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑f : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
    (⨅ (r : (↑(Ioi x) : Type)), (↑f : ℝ → ℝ) (↑r : ℝ))
have refine : BddBelow ((↑f : ℝ → ℝ) '' Ioi x)
Tactic: refine (Real.iInf_Ioi_eq_iInf_rat_gt _ ?_ f.mono).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
f : StieltjesFunction ℝ
x : ℝ
⊢ BddBelow ((↑f : ℝ → ℝ) '' Ioi x)
have refine : ∀ y ∈ (↑f : ℝ → ℝ) '' Ioi x, (↑f : ℝ → ℝ) x ≤ y
Tactic: refine ⟨f x, fun y => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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)
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
have obtain : ∀ (l u : ℝ) (hlu : rightLim f x ∈ Ioo l u) (lus : Ioo l u ⊆ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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) in 𝓝[≥] x, rightLim f y ∈ s
have pos : ∀ (hx : ∀ (y : R), y ≤ x), ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
Tactic: by_cases! hx : ∀ y, y ≤ x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
have neg : ∀ (hx : ∃ (y : R), x < y), ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
Tactic: by_cases! hx : ∀ y, y ≤ x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ y ∈ Ici x → rightLim f y ∈ s
have h : ∀ (hy : x ≤ y), rightLim f y ∈ s
Tactic: (hy : 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_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) in 𝓝[≥] x, rightLim f y ∈ s
have h : ∀ (y : R) (hy : x ≤ y), rightLim f y ∈ s
Tactic: filter_upwards [self_mem_nhdsWithin] with y (hy : 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_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 y ∈ s
have h : rightLim f x ∈ s
Tactic: rw [show y = x by exact le_antisymm (hx y) hy]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
have neg : ∀ (y₀ : R) (hy₀ : x < y₀), ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
Tactic: rcases hx with ⟨y₀, hy₀⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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) in 𝓝[≥] x, rightLim f y ∈ s
have neg : ∀ (y : R) (xy : x < y) (h'y : Ioo x y ⊆ f ⁻¹' Ioo l u), ∀ᶠ (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))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
have h : ∀ (z : R) (hz : z ∈ Ico x y), rightLim f z ∈ s
Tactic: filter_upwards [Ico_mem_nhdsGE xy] with z hz
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 ∈ s
have h : rightLim f z ∈ Ioo l u
Tactic: apply lus
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
have h : rightLim f z < u
Tactic: refine ⟨hlu.1.trans_le (hf.rightLim hz.1), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 < u
have h : ∀ (hz : x ∈ Ico x y), rightLim f x < u
Tactic: rcases hz.1.eq_or_lt with rfl | h''z
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ rightLim f z < u
have h₁ : ∀ (h''z : x < z), rightLim f z < u
Tactic: rcases hz.1.eq_or_lt with rfl | h''z
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ rightLim f z < u
have h : ∀ (h'z : 𝓝[>] z = ⊥), rightLim f z < u
Tactic: rcases Filter.eq_or_neBot (𝓝[>] z) with h'z | h'z
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ rightLim f z < u
have h₁ : ∀ (h'z : (𝓝[>] z).NeBot), rightLim f z < u
Tactic: rcases Filter.eq_or_neBot (𝓝[>] z) with h'z | h'z
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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 = ⊥
⊢ rightLim f z < u
have h : f z < u
Tactic: rw [rightLim_eq_of_eq_bot _ h'z]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
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 = ⊥
⊢ f z < u
have this : z ∈ Ioo x y
Tactic: have : z ∈ Ioo x y := ⟨h''z, hz.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ rightLim f z < u
have h : ∀ (a : R) (za : z < a) (ay : a < y), rightLim f z < u
Tactic: obtain ⟨a, za, ay⟩ : ∃ a : R, z < a ∧ a < y := Filter.nonempty_of_mem (Ioo_mem_nhdsGT hz.2)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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}
have refine : Subset.{u_1} (α := Set R) {x : R | leftLim (↑f : R → ℝ) x ≠ (↑f : R → ℝ) x} {x : R | ¬ContinuousAt (↑f : R → ℝ) x}
Tactic: refine Countable.mono ?_ f.mono.countable_not_continuousAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
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
⊢ False
have apply : leftLim (↑f : R → ℝ) x = (↑f : R → ℝ) x
Tactic: apply hx
-- 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
⊢ f.length ∅ = 0
have inl : ∀ (hR : IsEmpty R), f.length ∅ = 0
Tactic: rcases isEmpty_or_nonempty R with hR | hR
-- 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
inl : ∀ (hR : IsEmpty R), f.length ∅ = 0
⊢ f.length ∅ = 0
have inr : ∀ (hR : Nonempty R), f.length ∅ = 0
Tactic: rcases isEmpty_or_nonempty R with hR | hR
-- 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
hR : Nonempty R
⊢ f.length ∅ = 0
have inr : ∀ (inhabited_h : Inhabited R), f.length ∅ = 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
hR : Nonempty R
inhabited_h : Inhabited R
⊢ f.length ∅ = 0
have inr : Eq (α := ℝ≥0∞) (⨅ (a : R), ⨅ (b : R), ⨅ (_ : ∅ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)) 0
Tactic: rw [length_eq]
-- 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
a b : R
⊢ f.length (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have this : Nonempty R
Tactic: have : Nonempty R := ⟨a⟩
-- 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
a b : R
this : Nonempty R
⊢ f.length (Ioc a b) = ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a)
have 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)
Tactic: rw [length_eq]
-- 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
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)
have 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
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 ?_)
-- 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
a b : R
this : Nonempty R
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
have inl : ∀ (ab : b ≤ a), ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
Tactic: rcases le_or_gt b a with ab | ab
-- 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
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
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
have inr : ∀ (ab : a < b), ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
Tactic: rcases le_or_gt b a with ab | ab
-- 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
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
ab : b ≤ a
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
have inl : 0 ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
Tactic: rw [Real.toNNReal_of_nonpos (sub_nonpos.2 (f.mono ab))]
-- 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
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
ab : a < b
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
have h₁ : Ioc a b ⊆ Ioc a' b'
Tactic: simp only [Ioc_diff_botSet] at h
Cleared hypotheses: h
-- 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
a b : R
this : Nonempty R
a' b' : R
ab : a < b
h : Ioc a b ⊆ Ioc a' b'
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
have h₁ : b ≤ b'
Tactic: obtain ⟨h₁, h₂⟩ := (Ioc_subset_Ioc_iff ab).1 h
-- 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
a b : R
this : Nonempty R
a' b' : R
ab : a < b
h : Ioc a b ⊆ Ioc a' b'
h₁ : b ≤ b'
⊢ ((↑f : R → ℝ) b - (↑f : R → ℝ) a).toNNReal ≤ ((↑f : R → ℝ) b' - (↑f : R → ℝ) a').toNNReal
have h₂ : a' ≤ a
Tactic: obtain ⟨h₁, h₂⟩ := (Ioc_subset_Ioc_iff ab).1 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
s₁ s₂ : Set R
h : s₁ ⊆ s₂
⊢ f.length s₁ ≤ f.length s₂
have inl : ∀ (hR : IsEmpty R), f.length s₁ ≤ f.length s₂
Tactic: rcases isEmpty_or_nonempty R with hR | hR
-- 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
s₁ s₂ : Set R
h : s₁ ⊆ s₂
inl : ∀ (hR : IsEmpty R), f.length s₁ ≤ f.length s₂
⊢ f.length s₁ ≤ f.length s₂
have inr : ∀ (hR : Nonempty R), f.length s₁ ≤ f.length s₂
Tactic: rcases isEmpty_or_nonempty R with hR | hR
-- 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
s₁ s₂ : Set R
h : s₁ ⊆ s₂
hR : Nonempty R
⊢ f.length s₁ ≤ f.length s₂
have inr : LE.le (α := ℝ≥0∞) (⨅ (a : R), ⨅ (b : R), ⨅ (_ : s₁ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
  (⨅ (a : R), ⨅ (b : R), ⨅ (_ : s₂ \ botSet ⊆ Ioc a b), ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a))
Tactic: simp only [length_eq]
-- 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
s : Set R
⊢ f.length (s \ botSet) = f.length s
have inl : ∀ (hR : IsEmpty R), f.length (s \ botSet) = f.length s
Tactic: rcases isEmpty_or_nonempty R with hR | hR
-- 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
s : Set R
inl : ∀ (hR : IsEmpty R), f.length (s \ botSet) = f.length s
⊢ f.length (s \ botSet) = f.length s
have inr : ∀ (hR : Nonempty R), f.length (s \ botSet) = f.length s
Tactic: rcases isEmpty_or_nonempty R with hR | hR
-- 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
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ (i : ℕ), Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i) →
      ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have rcases : ∀ s ⊆ univ,
  ∀ (hf : s.Finite) (hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)),
    ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
Tactic: rcases isCompact_Icc.elim_finite_subcover_image
        (fun (i : ℕ) (_ : i ∈ univ) => @isOpen_Iotop _ _ _ _ (c i) (d i)) (by simpa using ss) with
      ⟨s, _, hf, hs⟩
-- 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
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ (i : ℕ), Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i) →
      ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
s : Set ℕ
left : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have e : Eq.{u_1 + 1} (α := Set R) (⋃ i ∈ (↑(hf.toFinset (s := s)) : Set ℕ), Iotop (c i) (d i)) (⋃ i ∈ s, Iotop (c i) (d i))
Tactic: have e : ⋃ i ∈ (hf.toFinset : Set ℕ), Iotop (c i) (d i) = ⋃ i ∈ s, Iotop (c i) (d i) := by
      simp only [Finset.set_biUnion_coe,
        Finite.mem_toFinset]
-- 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
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ (i : ℕ), Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ (↑s : Set ℕ), Iotop (c i) (d i) →
      ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑ i ∈ s, ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
s : Set ℕ
left : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)
e : Eq.{u_1 + 1} (α := Set R) (⋃ i ∈ (↑(hf.toFinset (s := s)) : Set ℕ), Iotop (c i) (d i)) (⋃ i ∈ s, Iotop (c i) (d i))
⊢ ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ∑' (i : ℕ), ofReal ((↑f : R → ℝ) (d i) - (↑f : R → ℝ) (c i))
have rw : ofReal ((↑f : R → ℝ) b - (↑f : R → ℝ) a) ≤ ⨆ (s : Finset ℕ), ∑ a ∈ s, ofReal ((↑f : R → ℝ) (d a) - (↑f : R → ℝ) (c a))
Tactic: rw [ENNReal.tsum_eq_iSup_sum]