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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
refine_2 :
  ∀ (b : E) (b_mem : b ∈ u) (hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))),
    ∃ b ∈ D, ‖(↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ)) - b‖ < ε
⊢ ∃ b ∈ D, ‖(↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ)) - b‖ < ε

Tactic:
have ⟨b, b_mem, hb⟩ := SeminormedAddCommGroup.mem_closure_iff.1 (dense_u a) _ approx_a_pos
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
linarith : ε / 3 ≤ 0 → 3 / 3 = 1
linarith₁ : ε / 3 ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ε / 3 ≤ 0 → GT.gt (α := ℝ) 3 0
linarith₃ : ε / 3 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 3 0) = 0
⊢ 0 < ε / 3

Tactic:
linarith [ε_pos]
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
refine_2 :
  ∀ (t : Set X) (ht : t ∈ 𝒜₀) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hst :
      ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ <
        ε / 3),
    ∃ b ∈ D, ‖(↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ)) - b‖ < ε
⊢ ∃ b ∈ D, ‖(↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ)) - b‖ < ε

Tactic:
rcases SeminormedAddCommGroup.mem_closure_iff.1
        (h𝒜₀.indicatorConstLp_subset_closure p b ⟨s, ms, hμs, rfl⟩)
          (ε / 3) (by linarith [ε_pos]) with ⟨-, ⟨t, ht, hμt, rfl⟩, hst⟩

Premises used: MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure, HDiv.hDiv, SeminormedAddCommGroup.mem_closure_iff, Exists.intro, Iff.mp, OfNat.ofNat, rfl
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
⊢ MeasurableSet t

Tactic:
have mt := h𝒜₀.measurable t ht
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
mt : MeasurableSet t
⊢ indicatorConstLp (s := t) p mt hμt b =
    key 1 (fun (x : Fin 1) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ u) b b_mem) fun (x : Fin 1) ↦
      Subtype.mk (p := fun (x : Set X) ↦ x ∈ 𝒜₀) t ht

Tactic:
simp [key]
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
mt : MeasurableSet t
refine_2 :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ))
        (indicatorConstLp (s := t) p mt hμt b)‖ <
    ε
⊢ ∃ b ∈ D, ‖(↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ)) - b‖ < ε

Tactic:
refine ⟨indicatorConstLp p mt hμt b,
        ⟨1, fun _ ↦ ⟨b, b_mem⟩, fun _ ↦ ⟨t, ht⟩, by simp [key]⟩, ?_⟩
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
mt : MeasurableSet t
refine_2 :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms ⋯ a) (indicatorConstLp (s := s) p ms hμs b) +
        HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p mt hμt b)‖ <
    ε / 2 + ε / 2
⊢ ‖HSub.hSub (α := ↥(Lp E p μ)) (↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ))
        (indicatorConstLp (s := t) p mt hμt b)‖ <
    ε

Tactic:
rw [Lp.simpleFunc.coe_indicatorConst,
        ← sub_add_sub_cancel _ (indicatorConstLp p ms hμs b), ← add_halves ε]

Premises used: sub_add_sub_cancel, add_halves, MeasureTheory.indicatorConstLp, MeasureTheory.Lp.simpleFunc.coe_indicatorConst
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
mt : MeasurableSet t
linarith : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → 2 / 2 = 1
linarith₁ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₂ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → 2 / 2 = 1
linarith₃ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₅ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₆ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₇ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₈ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → GT.gt (α := ℝ) 6 0
linarith₉ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → 3 / 3 = 1
linarith₁₀ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₁₁ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → GT.gt (α := ℝ) 3 0
linarith₁₂ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → 2 * (0 - ε) + (3 * ε + 3 * ε - (2 * ε + 2 * ε)) = 0
linarith₁₃ : ε / 2 + ε / 2 ≤ ε / 3 + ε / 3 → GT.gt (α := ℝ) 2 0
⊢ ε / 3 + ε / 3 < ε / 2 + ε / 2

Tactic:
linarith [ε_pos]
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
mt : MeasurableSet t
refine_2 :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms ⋯ a) (indicatorConstLp (s := s) p ms hμs b)‖ ≤ ε / 3
⊢ ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms ⋯ a) (indicatorConstLp (s := s) p ms hμs b) +
        HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p mt hμt b)‖ <
    ε / 2 + ε / 2

Tactic:
refine lt_of_le_of_lt (b := ε / 3 + ε / 3) (norm_add_le_of_le ?_ hst.le) (by linarith [ε_pos])

Premises used: lt_of_le_of_lt, LT.lt.le, norm_add_le_of_le
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
mt : MeasurableSet t
refine_2 : ‖a - b‖ * μ.real s ^ (1 / p.toReal) ≤ ε / 3
⊢ ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms ⋯ a) (indicatorConstLp (s := s) p ms hμs b)‖ ≤ ε / 3

Tactic:
rw [indicatorConstLp_sub, norm_indicatorConstLp p_ne_zero p_ne_top.elim]

Premises used: MeasureTheory.norm_indicatorConstLp, MeasureTheory.indicatorConstLp_sub, Fact.elim
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
mt : MeasurableSet t
⊢ ‖a - b‖ * μ.real s ^ (1 / p.toReal) ≤ ε / (3 * (1 + μ.real s ^ (1 / p.toReal))) * μ.real s ^ (1 / p.toReal)

Tactic:
mul_le_mul_of_nonneg_right (le_of_lt hb) μs_pow_nonneg

Premises used: le_of_lt, mul_le_mul_of_nonneg_right
-- 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}
a : E
s : Set X
ms : MeasurableSet s
hμs_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst :
  ‖HSub.hSub (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs b) (indicatorConstLp (s := t) p ⋯ hμt b)‖ < ε / 3
mt : MeasurableSet t
rw : ε / 3 * (μ.real s ^ (1 / p.toReal) / (1 + μ.real s ^ (1 / p.toReal))) ≤ ε / 3 * 1
⊢ ε / (3 * (1 + μ.real s ^ (1 / p.toReal))) * μ.real s ^ (1 / p.toReal) ≤ ε / 3

Tactic:
rw [← mul_one (ε / 3), div_mul_eq_div_mul_one_div, mul_assoc, one_div_mul_eq_div]

Premises used: mul_assoc, HDiv.hDiv, one_div_mul_eq_div, div_mul_eq_div_mul_one_div, mul_one, OfNat.ofNat