-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem Measure.MeasureDense.indicatorConstLp_subset_closure (h𝒜 : μ.MeasureDense 𝒜) (c : E) :
    {indicatorConstLp p hs hμs c | (s : Set X) (hs : MeasurableSet s) (hμs : μ s ≠ ∞)} ⊆
    closure {indicatorConstLp p (h𝒜.measurable s hs) hμs c |
      (s : Set X) (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞)}

Proof state:
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs c = x}

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs 0 = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs 0 = x}

case inr
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs c = x}

Proof state:
case inl
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs 0 = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs 0 = x}

Tactic:
refine Subset.trans ?_ subset_closure

Result:
case inl
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs 0 = x} ⊆
    {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs 0 = x}

Proof state:
case inr.intro.intro.intro.intro.intro.intro
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ dist (indicatorConstLp p ms hμs c) (indicatorConstLp p ⋯ hμt c) < ε

Tactic:
rw [dist_indicatorConstLp_eq_norm, norm_indicatorConstLp p_pos.ne.symm p_ne_top.elim]

Result:
case inr.intro.intro.intro.intro.intro.intro
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * (μ (s ∆ t)).toReal ^ (1 / p.toReal) < ε

Proof state:
case inl
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), indicatorConstLp p hs hμs 0 = x} ⊆
    {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs 0 = x}

Tactic:
rintro - ⟨s, ms, hμs, rfl⟩

Result:
case inl.intro.intro.intro
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ indicatorConstLp p ms hμs 0 ∈ {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), indicatorConstLp p ⋯ hμs 0 = x}

Proof state:
case inl.intro.intro.intro.intro.intro
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
⊢ indicatorConstLp p ⋯ hμt 0 = indicatorConstLp p ms hμs 0

Tactic:
simp_rw [indicatorConstLp]

Result:
case inl.intro.intro.intro.intro.intro
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 ≠ ⊤)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ⊤
⊢ MemLp.toLp (t.indicator fun x => 0) ⋯ = MemLp.toLp (s.indicator fun x => 0) ⋯