awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f g : X → E
hf : MemLp f p μ
hg : MemLp g p μ
f_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf - b‖ < ε
g_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp g hg - b‖ < ε
ε : ℝ
ε_pos : 0 < ε
bf : ↥(Lp E p μ)
hbf : ‖MemLp.toLp f hf - bf‖ < ε / 2
nf : ℕ
df : Fin nf → (↑u : Type u_2)
sf : Fin nf → (↑𝒜₀ : Type u_1)
bf_eq : bf = key nf df sf
bg : ↥(Lp E p μ)
hbg : ‖MemLp.toLp g hg - bg‖ < ε / 2
ng : ℕ
dg : Fin ng → (↑u : Type u_2)
sg : Fin ng → (↑𝒜₀ : Type u_1)
bg_eq : bg = key ng dg sg
d : (i : Fin (nf + ng)) → (↑u : Type u_2) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then df (i.castLT h) else dg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
s : (i : Fin (nf + ng)) → (↑𝒜₀ : Type u_1) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then sf (i.castLT h) else sg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
e_a : MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg) = MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)
⊢ ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ = ‖MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)‖

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f g : X → E
hf : MemLp f p μ
hg : MemLp g p μ
f_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf - b‖ < ε
g_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp g hg - b‖ < ε
ε : ℝ
ε_pos : 0 < ε
bf : ↥(Lp E p μ)
hbf : ‖MemLp.toLp f hf - bf‖ < ε / 2
nf : ℕ
df : Fin nf → (↑u : Type u_2)
sf : Fin nf → (↑𝒜₀ : Type u_1)
bf_eq : bf = key nf df sf
bg : ↥(Lp E p μ)
hbg : ‖MemLp.toLp g hg - bg‖ < ε / 2
ng : ℕ
dg : Fin ng → (↑u : Type u_2)
sg : Fin ng → (↑𝒜₀ : Type u_1)
bg_eq : bg = key ng dg sg
d : (i : Fin (nf + ng)) → (↑u : Type u_2) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then df (i.castLT h) else dg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
s : (i : Fin (nf + ng)) → (↑𝒜₀ : Type u_1) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then sf (i.castLT h) else sg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
⊢ MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg) = MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f g : X → E
hf : MemLp f p μ
hg : MemLp g p μ
f_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf - b‖ < ε
g_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp g hg - b‖ < ε
ε : ℝ
ε_pos : 0 < ε
bf : ↥(Lp E p μ)
hbf : ‖MemLp.toLp f hf - bf‖ < ε / 2
nf : ℕ
df : Fin nf → (↑u : Type u_2)
sf : Fin nf → (↑𝒜₀ : Type u_1)
bf_eq : bf = key nf df sf
bg : ↥(Lp E p μ)
hbg : ‖MemLp.toLp g hg - bg‖ < ε / 2
ng : ℕ
dg : Fin ng → (↑u : Type u_2)
sg : Fin ng → (↑𝒜₀ : Type u_1)
bg_eq : bg = key ng dg sg
d : (i : Fin (nf + ng)) → (↑u : Type u_2) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then df (i.castLT h) else dg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
s : (i : Fin (nf + ng)) → (↑𝒜₀ : Type u_1) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then sf (i.castLT h) else sg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
⊢ ‖MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)‖ ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖

Tactic:
norm_add_le ..

Premises used: norm_add_le, ENNReal.toReal, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f g : X → E
hf : MemLp f p μ
hg : MemLp g p μ
f_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf - b‖ < ε
g_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp g hg - b‖ < ε
ε : ℝ
ε_pos : 0 < ε
bf : ↥(Lp E p μ)
hbf : ‖MemLp.toLp f hf - bf‖ < ε / 2
nf : ℕ
df : Fin nf → (↑u : Type u_2)
sf : Fin nf → (↑𝒜₀ : Type u_1)
bf_eq : bf = key nf df sf
bg : ↥(Lp E p μ)
hbg : ‖MemLp.toLp g hg - bg‖ < ε / 2
ng : ℕ
dg : Fin ng → (↑u : Type u_2)
sg : Fin ng → (↑𝒜₀ : Type u_1)
bg_eq : bg = key ng dg sg
d : (i : Fin (nf + ng)) → (↑u : Type u_2) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then df (i.castLT h) else dg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
s : (i : Fin (nf + ng)) → (↑𝒜₀ : Type u_1) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then sf (i.castLT h) else sg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
linarith : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → 2 / 2 = 1
linarith₁ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → GT.gt (α := ℝ) 2 0
linarith₃ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → 2 / 2 = 1
linarith₄ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → GT.gt (α := ℝ) 2 0
linarith₆ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → 2 / 2 = 1
linarith₇ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → GT.gt (α := ℝ) 2 0
linarith₉ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → 2 / 2 = 1
linarith₁₀ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → GT.gt (α := ℝ) 2 0
linarith₁₂ :
  ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ →
    2 * ‖MemLp.toLp f hf - bf‖ - 1 * ε + (2 * ‖MemLp.toLp g hg - bg‖ - 1 * ε) +
        2 * (ε - (‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖)) =
      0
linarith₁₃ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → GT.gt (α := ℝ) 2 0
⊢ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ < ε

Tactic:
linarith [hbf, hbg]
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f g : X → E
hf : MemLp f p μ
hg : MemLp g p μ
f_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf - b‖ < ε
g_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp g hg - b‖ < ε
ε : ℝ
ε_pos : 0 < ε
bf : ↥(Lp E p μ)
hbf : ‖MemLp.toLp f hf - bf‖ < ε / 2
nf : ℕ
df : Fin nf → (↑u : Type u_2)
sf : Fin nf → (↑𝒜₀ : Type u_1)
bf_eq : bf = key nf df sf
bg : ↥(Lp E p μ)
hbg : ‖MemLp.toLp g hg - bg‖ < ε / 2
ng : ℕ
dg : Fin ng → (↑u : Type u_2)
sg : Fin ng → (↑𝒜₀ : Type u_1)
bg_eq : bg = key ng dg sg
d : (i : Fin (nf + ng)) → (↑u : Type u_2) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then df (i.castLT h) else dg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
s : (i : Fin (nf + ng)) → (↑𝒜₀ : Type u_1) :=
  fun (i : Fin (nf + ng)) ↦ if h : (↑i : ℕ) < nf then sf (i.castLT h) else sg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
f₁ : ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ = ‖MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)‖
f₂ : ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ < ε
⊢ ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ < ε

Tactic:
calc
          ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖
            = ‖(MemLp.toLp f hf) - bf + ((MemLp.toLp g hg) - bg)‖ := by congr; abel
          _ ≤ ‖(MemLp.toLp f hf) - bf‖ + ‖(MemLp.toLp g hg) - bg‖ := norm_add_le ..
          _ < ε := by linarith [hbf, hbg]

Premises used: HSub.hSub, norm_add_le, HAdd.hAdd, MeasureTheory.MemLp.toLp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
pos : ∀ (h : IsTop b), Ioc a b ⊆ Ioc a b
neg : ∀ (h : ¬IsTop b), Ioo a b ⊆ Ioc a b
⊢ (if IsTop b then Ioc a b else Ioo a b) ⊆ Ioc a b

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
h : IsTop b
⊢ Ioc a b ⊆ Ioc a b

Tactic:
simp [Ioo_subset_Ioc_self]

Premises used: Set.Ioo_subset_Ioc_self
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
h : ¬IsTop b
⊢ Ioo a b ⊆ Ioc a b

Tactic:
simp [Ioo_subset_Ioc_self]

Premises used: Set.Ioo_subset_Ioc_self
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
pos : ∀ (h : IsTop b), Ioo a b ⊆ Ioc a b
neg : ∀ (h : ¬IsTop b), Ioo a b ⊆ Ioo a b
⊢ Ioo a b ⊆ if IsTop b then Ioc a b else Ioo a b

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
h : IsTop b
⊢ Ioo a b ⊆ Ioc a b

Tactic:
simp [Ioo_subset_Ioc_self]

Premises used: Set.Ioo_subset_Ioc_self
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
h : ¬IsTop b
⊢ Ioo a b ⊆ Ioo a b

Tactic:
simp [Ioo_subset_Ioc_self]

Premises used: Set.Ioo_subset_Ioc_self
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
a b : R
pos : ∀ (h : IsTop b), IsOpen[inst_1] (Ioc a b)
neg : ∀ (h : ¬IsTop b), IsOpen[inst_1] (Ioo a b)
⊢ IsOpen[inst_1] (if IsTop b then Ioc a b else Ioo a b)

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
a b : R
h : IsTop b
x : R
hx : x ∈ Ioi a
⊢ x ∈ Ioc a b

Tactic:
⟨hx, h _⟩

Premises used: Set.Ioc, Set.Mem, setOf, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
a b : R
h : IsTop b
x : R
hx : x ∈ Ioi a
⊢ x ∈ Ioc a b

Tactic:
exact ⟨hx, h _⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
a b : R
h : IsTop b
⊢ Ioc a b = Ioi a

Tactic:
have : Ioc a b = Ioi a := Subset.antisymm (fun x hx ↦ hx.1) (fun x hx ↦ by exact ⟨hx, h _⟩)
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
a b : R
h : IsTop b
this : Ioc a b = Ioi a
⊢ IsOpen[inst_1] (Ioc a b)

Tactic:
simp [this, isOpen_Ioi]

Premises used: isOpen_Ioi
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
a b : R
h : ¬IsTop b
⊢ IsOpen[inst_1] (Ioo a b)

Tactic:
simp [isOpen_Ioo]

Premises used: isOpen_Ioo
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
rw : ∀ ⦃a_1 : R⦄, a_1 ∈ Ioc a b → ∀ ⦃b : R⦄, Membership.mem (γ := Set R) botSet b → a_1 ≠ b
⊢ Ioc a b \ botSet = Ioc a b

Tactic:
rw [sdiff_eq_left, disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne, sdiff_eq_left
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b c : R
hc : a < c
right : c ≤ b
hc' : Membership.mem (γ := Set R) botSet c
⊢ False

Tactic:
(hc' a).not_gt hc

Premises used: LE.le.not_gt
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
a b c : R
hc : a < c
right : c ≤ b
hc' : Membership.mem (γ := Set R) botSet c
⊢ False

Tactic:
exact (hc' a).not_gt hc

Premises used: LE.le.not_gt
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
x y : R
h : x < y
contrapose! : ∀ (h : Membership.mem (γ := Set R) botSet y), y ≤ x
⊢ y ∉ botSet

Tactic:
contrapose! h
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
x y : R
h : Membership.mem (γ := Set R) botSet y
⊢ y ≤ x

Tactic:
h x
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
x y : R
h : Membership.mem (γ := Set R) botSet y
⊢ y ≤ x

Tactic:
exact h x
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
⊢ Set.Subsingleton.{u_1} (α := R) botSet

Tactic:
subsingleton_isBot _

Premises used: botSet, Set.subsingleton_isBot
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : MeasurableSpace R
inst_2 : MeasurableSingletonClass R
⊢ MeasurableSet.{u_1} (α := R) botSet

Tactic:
subsingleton_botSet.measurableSet

Premises used: Set.Subsingleton.measurableSet, subsingleton_botSet
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
x : R
hx : IsBot x
⊢ Eq (α := Set R) botSet {x}

Tactic:
(subsingleton_botSet (R := R)).eq_singleton_of_mem hx

Premises used: Set.Subsingleton.eq_singleton_of_mem, subsingleton_botSet
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f g : StieltjesFunction R
h : ∀ (x : R), (↑f : R → ℝ) x = (↑g : R → ℝ) x
⊢ f = g

Tactic:
(StieltjesFunction.mk.injEq ..).mpr (funext h)

Premises used: Eq.mpr, StieltjesFunction.mk.injEq, funext
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f g : StieltjesFunction R
h : ∀ (x : R), (↑f : R → ℝ) x = (↑g : R → ℝ) x
⊢ f = g

Tactic:
exact (StieltjesFunction.mk.injEq ..).mpr (funext h)

Premises used: Eq.mpr, StieltjesFunction.mk.injEq, funext
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
⊢ Monotone (↑f : R → ℝ)

Tactic:
f.mono'

Premises used: StieltjesFunction.mono'
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
x : R
⊢ ContinuousWithinAt (↑f : R → ℝ) (Ici x) x

Tactic:
f.right_continuous' x

Premises used: StieltjesFunction.right_continuous'
-- 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
rw : ContinuousWithinAt (↑f : R → ℝ) (Ici x) x
⊢ rightLim (↑f : R → ℝ) x = (↑f : R → ℝ) x

Tactic:
rw [← f.mono.continuousWithinAt_Ioi_iff_rightLim_eq, continuousWithinAt_Ioi_iff_Ici]

Premises used: StieltjesFunction.mono, Monotone.continuousWithinAt_Ioi_iff_rightLim_eq, continuousWithinAt_Ioi_iff_Ici
-- 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
⊢ ContinuousWithinAt (↑f : R → ℝ) (Ici x) x

Tactic:
f.right_continuous' x

Premises used: StieltjesFunction.right_continuous'
-- 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
⊢ ContinuousWithinAt (↑f : R → ℝ) (Ici x) x

Tactic:
exact f.right_continuous' x

Premises used: StieltjesFunction.right_continuous'
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
rw₁ rw₂ : (↑f : R → ℝ) x = (↑f : R → ℝ) x
⊢ ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R) = (↑f : R → ℝ) x

Tactic:
rw [← this, f.rightLim_eq]

Premises used: StieltjesFunction.rightLim_eq
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
suffices : 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

Tactic:
suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.rightLim_eq]
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
rw : 𝓝[>] x ≠ ⊥
⊢ rightLim (↑f : R → ℝ) x = ⨅ (r : (↑(Ioi x) : Type u_1)), (↑f : R → ℝ) (↑r : R)

Tactic:
rw [f.mono.rightLim_eq_sInf, sInf_image']

Premises used: Monotone.rightLim_eq_sInf, StieltjesFunction.mono, sInf_image'
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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
rw : (𝓝[>] x).NeBot
⊢ 𝓝[>] x ≠ ⊥

Tactic:
rw [← neBot_iff]

Premises used: Filter.neBot_iff
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
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).NeBot

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
f : StieltjesFunction ℝ
x : ℝ
rw :
  Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑f : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
    (⨅ (r : (↑(Ioi x) : Type)), (↑f : ℝ → ℝ) (↑r : ℝ))
⊢ ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑f : ℝ → ℝ) (↑(↑r : ℚ) : ℝ) = (↑f : ℝ → ℝ) x

Tactic:
rw [← iInf_Ioi_eq f x]

Premises used: StieltjesFunction.iInf_Ioi_eq
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
f : StieltjesFunction ℝ
x : ℝ
⊢ Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑f : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
    (⨅ (r : (↑(Ioi x) : Type)), (↑f : ℝ → ℝ) (↑r : ℝ))

Tactic:
(Real.iInf_Ioi_eq_iInf_rat_gt _ ?_ f.mono).symm

Premises used: Real.iInf_Ioi_eq_iInf_rat_gt, StieltjesFunction.mono, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
f : StieltjesFunction ℝ
x : ℝ
refine : BddBelow ((↑f : ℝ → ℝ) '' Ioi x)
⊢ Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑f : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
    (⨅ (r : (↑(Ioi x) : Type)), (↑f : ℝ → ℝ) (↑r : ℝ))

Tactic:
refine (Real.iInf_Ioi_eq_iInf_rat_gt _ ?_ f.mono).symm

Premises used: Real.iInf_Ioi_eq_iInf_rat_gt, StieltjesFunction.mono, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
f : StieltjesFunction ℝ
x : ℝ
⊢ BddBelow ((↑f : ℝ → ℝ) '' Ioi x)

Tactic:
⟨f x, fun y => ?_⟩

Premises used: StieltjesFunction.toFun, Set.Nonempty, BddBelow, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
f : StieltjesFunction ℝ
x : ℝ
refine : ∀ y ∈ (↑f : ℝ → ℝ) '' Ioi x, (↑f : ℝ → ℝ) x ≤ y
⊢ BddBelow ((↑f : ℝ → ℝ) '' Ioi x)

Tactic:
refine ⟨f x, fun y => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
f : StieltjesFunction ℝ
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ (↑f : ℝ → ℝ) x ≤ (↑f : ℝ → ℝ) y

Tactic:
f.mono (le_of_lt hy_mem)

Premises used: le_of_lt, StieltjesFunction.mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
f : StieltjesFunction ℝ
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ (↑f : ℝ → ℝ) x ≤ (↑f : ℝ → ℝ) y

Tactic:
exact f.mono (le_of_lt hy_mem)

Premises used: le_of_lt, StieltjesFunction.mono
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
x : ℝ
⊢ leftLim (↑StieltjesFunction.id : ℝ → ℝ) x = x

Tactic:
continuousWithinAt_id.leftLim_eq

Premises used: continuousWithinAt_id, ContinuousWithinAt.leftLim_eq
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f : StieltjesFunction R
c : ℝ
x x_1 : R
⊢ x ≤ x_1 → LE.le (α := ℝ) ((fun (x : R) ↦ c) x) ((fun (x : R) ↦ c) x_1)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
c : ℝ
x : R
⊢ (↑(StieltjesFunction.const R c) : R → ℝ) x = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
x : R
⊢ (↑0 : R → ℝ) x = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Stieltjes
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : TopologicalSpace R
f g : StieltjesFunction R
x : R
⊢ (↑(f + g) : R → ℝ) x = (↑f : R → ℝ) x + (↑g : R → ℝ) x

Tactic:
rfl

Premises used: 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 : ℝ), rightLim f x ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
mem_nhds_iff_exists_Ioo_subset.1 hs

Premises used: Set.Mem, Iff.mp, mem_nhds_iff_exists_Ioo_subset