-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem boundedContinuousFunction_dense [SecondCountableTopologyEither α E] [Fact (1 ≤ p)]
    (hp : p ≠ ∞) [μ.WeaklyRegular] :
    Dense (boundedContinuousFunction E p μ : Set (Lp E p μ))

Proof state:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
⊢ f ∈ closure ↑(boundedContinuousFunction E p μ)

Tactic:
refine (mem_closure_iff_nhds_basis EMetric.nhds_basis_closed_eball).2 fun ε hε ↦ ?_

Result:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ EMetric.closedBall f ε

Proof state:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
⊢ Dense ↑(boundedContinuousFunction E p μ)

Tactic:
intro f

Result:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
⊢ f ∈ closure ↑(boundedContinuousFunction E p μ)

Proof state:
case intro.intro
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ MemLp.toLp (⇑g) g_mem ∈ EMetric.closedBall f ε

Tactic:
rwa [EMetric.mem_closedBall', ← Lp.toLp_coeFn f (Lp.memLp f), Lp.edist_toLp_toLp]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ ∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ EMetric.closedBall f ε

Tactic:
refine ⟨g_mem.toLp _, ⟨g, rfl⟩, ?_⟩

Result:
case intro.intro
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ MemLp.toLp (⇑g) g_mem ∈ EMetric.closedBall f ε

Proof state:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ EMetric.closedBall f ε

Tactic:
obtain ⟨g, hg, g_mem⟩ :
    ∃ g : α →ᵇ E, eLpNorm ((f : α → E) - (g : α → E)) p μ ≤ ε ∧ MemLp g p μ :=
  (Lp.memLp f).exists_boundedContinuous_eLpNorm_sub_le hp hε.ne'

Result:
case intro.intro
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ ∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ EMetric.closedBall f ε