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}
⊢ SeparableSpace ↥(Lp E p μ)

Tactic:
⟨D, ?_, ?_⟩

Premises used: And.intro, Exists.intro, TopologicalSpace.SeparableSpace.mk
-- 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}
refine_1 : D.Countable
refine_2 : Dense D
⊢ SeparableSpace ↥(Lp E p μ)

Tactic:
refine ⟨D, ?_, ?_⟩
-- 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 : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
⊢ Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)

Tactic:
have := count_𝒜₀.to_subtype
-- 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 : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
⊢ Countable.{u_2 + 1} (↑u : Type u_2)

Tactic:
have := countable_u.to_subtype
-- 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 : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this_1 : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
this : Countable.{u_2 + 1} (↑u : Type u_2)
n : ℕ
d : Fin n → (↑u : Type u_2)
s : Fin n → (↑𝒜₀ : Type u_1)
w : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))
h :
  f (Sigma.mk (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) n (d, s)) =
    key n d s
⊢ key n d s ∈ range f

Tactic:
use ⟨n, (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 : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this_1 : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
this : Countable.{u_2 + 1} (↑u : Type u_2)
⊢ D ⊆ range f

Tactic:
have : D ⊆ range f := by
      rintro - ⟨n, d, s, rfl⟩
      use ⟨n, (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 : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this_1 : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
this_2 : Countable.{u_2 + 1} (↑u : Type u_2)
this : D ⊆ range f
⊢ D.Countable

Tactic:
(countable_range f).mono this

Premises used: Set.countable_range, Set.Countable.mono
-- 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 : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this_1 : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
this_2 : Countable.{u_2 + 1} (↑u : Type u_2)
this : D ⊆ range f
⊢ D.Countable

Tactic:
exact (countable_range f).mono this

Premises used: Set.countable_range, Set.Countable.mono
-- 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}
⊢ Dense D

Tactic:
Lp.induction p_ne_top.elim (motive := fun f ↦ f ∈ closure D) ?_ ?_ isClosed_closure

Premises used: Membership.mem, Dense, closure, Fact.elim, MeasureTheory.Lp.induction, isClosed_closure
-- 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}
refine_2 :
  ∀ (c : E) {s : Set X} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (f : ↥(Lp E p μ)) ↦ f ∈ closure D) (↑(simpleFunc.indicatorConst p (s := s) hs ⋯ c) : ↥(Lp E p μ))
refine_2₁ :
  ∀ ⦃f g : X → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun (f : ↥(Lp E p μ)) ↦ f ∈ closure D) (MemLp.toLp f hf) →
        (fun (f : ↥(Lp E p μ)) ↦ f ∈ closure D) (MemLp.toLp g hg) →
          (fun (f : ↥(Lp E p μ)) ↦ f ∈ closure D) (MemLp.toLp f hf + MemLp.toLp g hg)
⊢ Dense D

Tactic:
refine Lp.induction p_ne_top.elim (motive := fun f ↦ f ∈ closure D) ?_ ?_ isClosed_closure

Premises used: Membership.mem, closure, Fact.elim, MeasureTheory.Lp.induction, isClosed_closure
-- 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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply ne_of_lt at hμs

Premises used: ne_of_lt
-- 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∞)
refine_2 : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖(↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ)) - b‖ < ε
⊢ (↑(simpleFunc.indicatorConst p (s := s) ms ⋯ a) : ↥(Lp E p μ)) ∈ closure D

Tactic:
rw [SeminormedAddCommGroup.mem_closure_iff]

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}
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 < ε
⊢ 0 ≤ μ.real s ^ (1 / p.toReal)

Tactic:
positivity
-- 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 < ε
⊢ 0 ≤ μ.real s ^ (1 / p.toReal)

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

Tactic:
have approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal))) :=
        div_pos ε_pos (by linarith [μs_pow_nonneg])