awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ ∃ b ∈ D, ‖MemLp.toLp f hf + MemLp.toLp g hg - b‖ < ε
have refine_2 : ∀ (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), ∃ b ∈ D, ‖MemLp.toLp f hf + MemLp.toLp g hg - b‖ < ε
Tactic: rcases g_mem (ε / 2) (by linarith [ε_pos]) with ⟨bg, ⟨ng, dg, sg, bg_eq⟩, hbg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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) ⋯)
⊢ ∃ b ∈ D, ‖MemLp.toLp f hf + MemLp.toLp g hg - b‖ < ε
have refine_2 : bf + bg = key (nf + ng) d s
Tactic: refine ⟨bf + bg, ⟨nf + ng, d, s, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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) ⋯)
refine_2 : bf + bg = key (nf + ng) d s
⊢ ∃ b ∈ D, ‖MemLp.toLp f hf + MemLp.toLp g hg - b‖ < ε
have refine_2₁ : ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ < ε
Tactic: refine ⟨bf + bg, ⟨nf + ng, d, s, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)‖
have e_a : MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg) = MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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‖ < ε
have linarith : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → 2 / 2 = 1
Tactic: linarith [hbf, hbg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ < ε
have linarith₁ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hbf, hbg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ < ε
have linarith₂ : ε ≤ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith [hbf, hbg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ < ε
have 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
Tactic: linarith [hbf, hbg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)‖ < ε
have f₁ : ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ = ‖MemLp.toLp f hf - bf + (MemLp.toLp g hg - 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)‖
⊢ ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ < ε
have f₂ : ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
⊢ (if IsTop b then Ioc a b else Ioo a b) ⊆ Ioc a b
have pos : ∀ (h : IsTop b), Ioc a b ⊆ Ioc a b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
pos : ∀ (h : IsTop b), Ioc a b ⊆ Ioc a b
⊢ (if IsTop b then Ioc a b else Ioo a b) ⊆ Ioc a b
have neg : ∀ (h : ¬IsTop b), Ioo a b ⊆ Ioc a b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
⊢ Ioo a b ⊆ if IsTop b then Ioc a b else Ioo a b
have pos : ∀ (h : IsTop b), Ioo a b ⊆ Ioc a b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
pos : ∀ (h : IsTop b), Ioo a b ⊆ Ioc a b
⊢ Ioo a b ⊆ if IsTop b then Ioc a b else Ioo a b
have neg : ∀ (h : ¬IsTop b), Ioo a b ⊆ Ioo a b
Tactic: split_ifs with h
-- 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
a b : R
⊢ IsOpen[inst_1] (if IsTop b then Ioc a b else Ioo a b)
have pos : ∀ (h : IsTop b), IsOpen[inst_1] (Ioc a b)
Tactic: split_ifs with h
-- 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
a b : R
pos : ∀ (h : IsTop b), IsOpen[inst_1] (Ioc a b)
⊢ IsOpen[inst_1] (if IsTop b then Ioc a b else Ioo a b)
have neg : ∀ (h : ¬IsTop b), IsOpen[inst_1] (Ioo a b)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (hypothesis)
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] (Ioc a b)
have this : 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 _⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
a b : R
⊢ Ioc a b \ botSet = Ioc a b
have rw : ∀ ⦃a_1 : R⦄, a_1 ∈ Ioc a b → ∀ ⦃b : R⦄, Membership.mem (γ := Set R) botSet b → a_1 ≠ b
Tactic: rw [sdiff_eq_left, disjoint_iff_forall_ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Stieltjes (goal)
Goal:
R : Type u_1
inst : LinearOrder R
x y : R
h : x < y
⊢ y ∉ botSet
have contrapose! : ∀ (h : Membership.mem (γ := Set R) botSet y), y ≤ x
Tactic: contrapose! h
Cleared hypotheses: h
-- 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
⊢ rightLim (↑f : R → ℝ) x = (↑f : R → ℝ) x
have rw : ContinuousWithinAt (↑f : R → ℝ) (Ici x) x
Tactic: rw [← f.mono.continuousWithinAt_Ioi_iff_rightLim_eq, continuousWithinAt_Ioi_iff_Ici]