awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
rcases :
  ∀ (f : α → E) (f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f)
    (I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ)
    (f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖) (f_mem : MemLp f p μ),
    ∃ (g : α → E),
      eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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⟩

Premises used: Set.subset_univ, isOpen_univ, LT.lt.ne', LT.lt.ne, MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
⊢ eLpNorm
      ((f - s.indicator fun (x : α) ↦ c) +
        HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c))
      p μ ≤
    ε

Tactic:
(hδ _ _
          (f_mem.aestronglyMeasurable.sub
            (aestronglyMeasurable_const.indicator s_closed.measurableSet))
          ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub
            (aestronglyMeasurable_const.indicator ht))
          I2 I1).le

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.sub, IsClosed.measurableSet, LT.lt.le, MeasureTheory.AEStronglyMeasurable.indicator, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
h :
  (f - t.indicator fun (_y : α) ↦ c) =
    (f - s.indicator fun (x : α) ↦ c) +
      HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
⊢ eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε

Tactic:
convert!
      (hδ _ _
          (f_mem.aestronglyMeasurable.sub
            (aestronglyMeasurable_const.indicator s_closed.measurableSet))
          ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub
            (aestronglyMeasurable_const.indicator ht))
          I2 I1).le using 2

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.sub, IsClosed.measurableSet, LT.lt.le, MeasureTheory.AEStronglyMeasurable.indicator, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
⊢ (f - t.indicator fun (_y : α) ↦ c) =
    (f - s.indicator fun (x : α) ↦ c) +
      HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)

Tactic:
simp only [sub_add_sub_cancel]

Premises used: sub_add_sub_cancel
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
⊢ eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε

Tactic:
have I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε := by
    convert!
      (hδ _ _
          (f_mem.aestronglyMeasurable.sub
            (aestronglyMeasurable_const.indicator s_closed.measurableSet))
          ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub
            (aestronglyMeasurable_const.indicator ht))
          I2 I1).le using 2
    simp only [sub_add_sub_cancel]
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)

Tactic:
⟨f, I3, f_cont, f_mem, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
refine : IsBounded (range f)
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)

Tactic:
refine ⟨f, I3, f_cont, f_mem, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
⊢ IsBounded (range f)

Tactic:
(BoundedContinuousFunction.ofNormedAddCommGroup f f_cont _ f_bound).isBounded_range

Premises used: BoundedContinuousFunction.isBounded_range, BoundedContinuousFunction.ofNormedAddCommGroup
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
hp : p ≠ ∞
f_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥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 α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
⊢ IsBounded (range f)

Tactic:
exact (BoundedContinuousFunction.ofNormedAddCommGroup f f_cont _ f_bound).isBounded_range

Premises used: BoundedContinuousFunction.isBounded_range, BoundedContinuousFunction.ofNormedAddCommGroup
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
⊢ 0 < ε ^ (1 / p)

Tactic:
have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ENNReal.ofReal (ε ^ (1 / p)) ≠ 0

Tactic:
simp only [Ne, ENNReal.ofReal_eq_zero, not_le, I]

Premises used: not_le, ENNReal.ofReal_eq_zero, Ne
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ENNReal.ofReal (ε ^ (1 / p)) ≠ 0

Tactic:
have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0 := by
    simp only [Ne, ENNReal.ofReal_eq_zero, not_le, I]
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ENNReal.ofReal p ≠ 0

Tactic:
simpa only [Ne, ENNReal.ofReal_eq_zero, not_le] using hp

Premises used: not_le, ENNReal.ofReal_eq_zero, Ne
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ENNReal.ofReal p ≠ 0

Tactic:
have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne, ENNReal.ofReal_eq_zero, not_le] using hp
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
rcases :
  ∀ (g : α →ᵇ E) (hg : eLpNorm (f - (⇑g : (a : α) → E)) (↑p.toNNReal : ℝ≥0∞) μ ≤ ENNReal.ofReal (ε ^ (1 / p)))
    (g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ),
    ∃ (g : α →ᵇ E),
      ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
        MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ

Tactic:
rcases hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.coe_ne_top A with ⟨g, hg, g_mem⟩

Premises used: MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
hg : eLpNorm (f - (⇑g : (a : α) → E)) (↑p.toNNReal : ℝ≥0∞) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ
⊢ eLpNorm (f - (⇑g : (a : α) → E)) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))

Tactic:
change eLpNorm _ (ENNReal.ofReal p) _ ≤ _ at hg

Premises used: ENNReal.ofReal, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ
hg : eLpNorm (f - (⇑g : (a : α) → E)) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ

Tactic:
⟨g, ?_, g_mem⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ
hg : eLpNorm (f - (⇑g : (a : α) → E)) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
refine : ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε
⊢ ∃ (g : α →ᵇ E),
    ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε ∧
      MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (ENNReal.ofReal p) μ

Tactic:
refine ⟨g, ?_, g_mem⟩
-- Module: Mathlib.MeasureTheory.Function.ContinuousMapDense
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NormalSpace α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
E : Type u_2
inst_4 : NormedAddCommGroup E
μ : Measure α
inst_5 : NormedSpace ℝ E
inst_6 : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α →ᵇ E
g_mem : MemLp.{u_1, u_2} (ε := E) (⇑g : (a : α) → E) (↑p.toNNReal : ℝ≥0∞) μ
hg : eLpNorm (f - (⇑g : (a : α) → E)) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
rwa :
  ∀ (hg : HPow.hPow (α := ℝ) (∫ (a : α), ‖HSub.hSub (β := α → E) f (⇑g : (a : α) → E) a‖ ^ p ∂μ) p⁻¹ ≤ ε ^ p⁻¹),
    LE.le (α := ℝ) 0 (∫ (a : α), ‖HSub.hSub (β := α → E) f (⇑g : (a : α) → E) a‖ ^ p ∂μ)
⊢ ∫ (x : α), ‖HSub.hSub (β := E) (f x) ((g : (a : α) → E) x : E)‖ ^ p ∂μ ≤ ε

Tactic:
rwa [(hf.sub g_mem).eLpNorm_eq_integral_rpow_norm B ENNReal.coe_ne_top,
    ENNReal.ofReal_le_ofReal_iff I.le, one_div, ENNReal.toReal_ofReal hp.le,
    Real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg

Premises used: Iff.mpr, ENNReal.ofReal_le_ofReal_iff, inv_pos, LT.lt.le, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm, ENNReal.toReal_ofReal, one_div, Real.rpow_le_rpow_iff, MeasureTheory.MemLp.sub, ENNReal.coe_ne_top