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)))
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 : 1 + μ.real s ^ (1 / p.toReal) ≤ 0 → 3 / 3 = 1
linarith₁ : 1 + μ.real s ^ (1 / p.toReal) ≤ 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : 1 + μ.real s ^ (1 / p.toReal) ≤ 0 → GT.gt (α := ℝ) 3 0
linarith₃ :
  1 + μ.real s ^ (1 / p.toReal) ≤ 0 →
    -1 + (HMul.hMul (α := ℝ) 1 0 - 1 * μ.real s ^ (1 / p.toReal)) +
        (HMul.hMul (α := ℝ) 1 1 + 1 * μ.real s ^ (1 / p.toReal) - HMul.hMul (α := ℝ) 1 0) =
      0
⊢ 0 < 1 + μ.real s ^ (1 / p.toReal)

Tactic:
linarith [μs_pow_nonneg]
-- 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 : 1 + μ.real s ^ (1 / p.toReal) < μ.real s ^ (1 / p.toReal) → 3 / 3 = 1
linarith₁ : 1 + μ.real s ^ (1 / p.toReal) < μ.real s ^ (1 / p.toReal) → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : 1 + μ.real s ^ (1 / p.toReal) < μ.real s ^ (1 / p.toReal) → GT.gt (α := ℝ) 3 0
linarith₃ :
  1 + μ.real s ^ (1 / p.toReal) < μ.real s ^ (1 / p.toReal) →
    -1 + (HMul.hMul (α := ℝ) 1 1 + 1 * μ.real s ^ (1 / p.toReal) - 1 * μ.real s ^ (1 / p.toReal)) = 0
⊢ μ.real s ^ (1 / p.toReal) ≤ 1 + μ.real s ^ (1 / p.toReal)

Tactic:
linarith
-- 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 : ε / 3 < 0 → 3 / 3 = 1
linarith₁ : ε / 3 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ε / 3 < 0 → GT.gt (α := ℝ) 3 0
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)))
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
⊢ ε / 3 * (μ.real s ^ (1 / p.toReal) / (1 + μ.real s ^ (1 / p.toReal))) ≤ ε / 3 * 1

Tactic:
exact mul_le_mul_of_nonneg_left
              ((div_le_one (by linarith [μs_pow_nonneg])).2 (by linarith))
              (by linarith [ε_pos])

Premises used: Iff.mpr, div_le_one, mul_le_mul_of_nonneg_left
-- 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
s₁ : ε / (3 * (1 + μ.real s ^ (1 / p.toReal))) * μ.real s ^ (1 / p.toReal) ≤ ε / 3
⊢ ‖a - b‖ * μ.real s ^ (1 / p.toReal) ≤ ε / 3

Tactic:
calc
        ‖a - b‖ * μ.real s ^ (1 / p.toReal)
          ≤ (ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))) * μ.real s ^ (1 / p.toReal) :=
              mul_le_mul_of_nonneg_right (le_of_lt hb) μs_pow_nonneg
        _ ≤ ε / 3 := by
            rw [← mul_one (ε / 3), div_mul_eq_div_mul_one_div, mul_assoc, one_div_mul_eq_div]
            exact mul_le_mul_of_nonneg_left
              ((div_le_one (by linarith [μs_pow_nonneg])).2 (by linarith))
              (by linarith [ε_pos])

Premises used: HMul.hMul, MeasureTheory.Measure.real, le_of_lt, HDiv.hDiv, mul_le_mul_of_nonneg_right, ENNReal.toReal, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- 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 : MemLp.toLp f hf ∈ closure D
g_mem : MemLp.toLp g hg ∈ closure D
refine_2 :
  ∀ (f_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf - b‖ < ε)
    (g_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp g hg - b‖ < ε) (ε : ℝ),
    0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf + MemLp.toLp g hg - b‖ < ε
⊢ MemLp.toLp f hf + MemLp.toLp g hg ∈ closure D

Tactic:
rw [SeminormedAddCommGroup.mem_closure_iff] at *

Premises used: SeminormedAddCommGroup.mem_closure_iff
-- 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 < ε
linarith : ε / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : ε / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : ε / 2 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 < ε / 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}
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 < ε
refine_2 :
  ∀ (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‖ < ε
⊢ ∃ b ∈ D, ‖MemLp.toLp f hf + MemLp.toLp g hg - b‖ < ε

Tactic:
rcases f_mem (ε / 2) (by linarith [ε_pos]) with ⟨bf, ⟨nf, df, sf, bf_eq⟩, hbf⟩

Premises used: HDiv.hDiv, OfNat.ofNat
-- 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
linarith : ε / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : ε / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : ε / 2 ≤ 0 → 2 / 2 = 1
linarith₄ : ε / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ε / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₆ : ε / 2 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 < ε / 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}
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
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‖ < ε
⊢ ∃ 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⟩

Premises used: HDiv.hDiv, OfNat.ofNat
-- 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) ⋯)
⊢ ∃ b ∈ D, ‖MemLp.toLp f hf + MemLp.toLp g hg - b‖ < ε

Tactic:
⟨bf + bg, ⟨nf + ng, d, s, ?_⟩, ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro
-- 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) ⋯)
refine_2 : bf + bg = key (nf + ng) d s
refine_2₁ : ‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ < ε
⊢ ∃ b ∈ D, ‖MemLp.toLp f hf + MemLp.toLp g hg - b‖ < ε

Tactic:
refine ⟨bf + bg, ⟨nf + ng, d, s, ?_⟩, ?_⟩
-- 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) ⋯)
⊢ bf + bg = key (nf + ng) d s

Tactic:
simp [key, d, s, Fin.sum_univ_add, bf_eq, bg_eq]

Premises used: Fin.sum_univ_add