-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem MemLp.exists_boundedContinuous_eLpNorm_sub_le [μ.WeaklyRegular] (hp : p ≠ ∞) {f : α → E}
    (hf : MemLp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ g : α →ᵇ E, eLpNorm (f - (g : α → E)) p μ ≤ ε ∧ MemLp g p μ

Proof state:
case intro.intro.intro.intro.intro.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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : μ (t \ s) < ↑η
hsμ : μ s < ⊤
I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ
⊢ ∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ ∧ IsBounded (range g)

Tactic:
rcases exists_continuous_eLpNorm_sub_le_of_closed hp s_closed isOpen_univ (subset_univ _) hsμ.ne c
    δpos.ne' with
  ⟨f, f_cont, I2, f_bound, -, f_mem⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f✝ : α → E
hf : MemLp f✝ p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : μ (t \ s) < ↑η
hsμ : μ s < ⊤
I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ
f : α → E
f_cont : Continuous f
I2 : eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
⊢ ∃ g, eLpNorm (g - t.indicator fun x => c) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ ∧ IsBounded (range g)

Proof state:
case intro.intro.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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous f
f_mem : MemLp f p μ
f_bd : IsBounded (range f)
g_cont : Continuous g
g_mem : MemLp g p μ
g_bd : IsBounded (range g)
f' : α →ᵇ E := { toFun := f, continuous_toFun := f_cont, map_bounded' := ⋯ }
g' : α →ᵇ E := { toFun := g, continuous_toFun := g_cont, map_bounded' := ⋯ }
⊢ IsBounded (range (f + g))

Tactic:
exact (f' + g').isBounded_range

Result:
no goals

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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : μ (t \ s) < ↑η
hsμ : μ s < ⊤
⊢ eLpNorm ((t \ s).indicator fun _y => c) p μ ≤ δ

Tactic:
exact hη _ μs.le

Result:
no goals

Proof state:
case intro.intro.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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous f
f_mem : MemLp f p μ
f_bd : IsBounded (range f)
g_cont : Continuous g
g_mem : MemLp g p μ
g_bd : IsBounded (range g)
⊢ IsBounded (range (f + g))

Tactic:
let f' : α →ᵇ E := ⟨⟨f, f_cont⟩, Metric.isBounded_range_iff.1 f_bd⟩

Result:
case intro.intro.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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f✝ : α → E
hf : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous f
f_mem : MemLp f p μ
f_bd : IsBounded (range f)
g_cont : Continuous g
g_mem : MemLp g p μ
g_bd : IsBounded (range g)
f' : α →ᵇ E := { toFun := f, continuous_toFun := f_cont, map_bounded' := ⋯ }
⊢ IsBounded (range (f + g))

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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : μ (t \ s) < ↑η
hsμ : μ s < ⊤
⊢ eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ

Tactic:
rw [← eLpNorm_neg, neg_sub, ← indicator_diff st]

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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : μ (t \ s) < ↑η
hsμ : μ s < ⊤
⊢ eLpNorm ((t \ s).indicator fun _y => c) 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✝ : μ.WeaklyRegular
hp : p ≠ ⊤
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f : α → E), Continuous f ∧ MemLp f p μ ∧ IsBounded (range f) → AEStronglyMeasurable f μ

Tactic:
exact fun f ⟨_, h, _⟩ => h.aestronglyMeasurable

Result:
no goals