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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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 ⊆ t, IsCompact s ∧ IsClosed[inst] s ∧ (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)

Tactic:
ht.exists_isCompact_isClosed_diff_lt htμ.ne hη_pos'.ne'

Premises used: MeasurableSet.exists_isCompact_isClosed_diff_lt, LT.lt.ne', LT.lt.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 α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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∞)
obtain :
  ∀ (s : Set α) (st : s ⊆ t) (s_compact : IsCompact s) (s_closed : IsClosed[inst] s)
    (μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)),
    ∃ (g : α → E),
      eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g

Tactic:
obtain ⟨s, st, s_compact, s_closed, μs⟩ :
      ∃ s, s ⊆ t ∧ IsCompact s ∧ IsClosed s ∧ μ (t \ s) < η :=
    ht.exists_isCompact_isClosed_diff_lt htμ.ne hη_pos'.ne'

Premises used: MeasurableSet.exists_isCompact_isClosed_diff_lt, LT.lt.ne', LT.lt.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 α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hsμ : μ s < ∞ := (measure_mono st).trans_lt htμ
-- 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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : eLpNorm.{u_1, u_2} (ε := E) ((t \ s).indicator fun (_y : α) ↦ c) p μ ≤ δ
⊢ eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ

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

Premises used: neg_sub, MeasureTheory.eLpNorm_neg, Set.indicator_diff
-- 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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ eLpNorm.{u_1, u_2} (ε := E) ((t \ s).indicator fun (_y : α) ↦ c) p μ ≤ δ

Tactic:
hη _ μs.le

Premises used: LT.lt.le
-- 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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ eLpNorm.{u_1, u_2} (ε := E) ((t \ s).indicator fun (_y : α) ↦ c) p μ ≤ δ

Tactic:
exact hη _ μs.le

Premises used: LT.lt.le
-- 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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ

Tactic:
have I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ := by
    rw [← eLpNorm_neg, neg_sub, ← indicator_diff st]
    exact hη _ μs.le
-- 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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
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 μ ≤ δ
⊢ ∃ (k : Set α), IsCompact k ∧ s ⊆ interior k

Tactic:
exists_compact_superset s_compact

Premises used: exists_compact_superset
-- 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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
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 μ ≤ δ
obtain :
  ∀ (k : Set α) (k_compact : IsCompact k) (sk : s ⊆ interior k),
    ∃ (g : α → E),
      eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g

Tactic:
obtain ⟨k, k_compact, sk⟩ : ∃ k : Set α, IsCompact k ∧ s ⊆ interior k :=
    exists_compact_superset s_compact

Premises used: exists_compact_superset, Set
-- 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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
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 μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
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_support : Function.support f ⊆ interior k) (f_mem : MemLp f p μ),
    ∃ (g : α → E),
      eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g

Tactic:
rcases exists_continuous_eLpNorm_sub_le_of_closed hp s_closed isOpen_interior sk hsμ.ne c δpos.ne'
    with ⟨f, f_cont, I2, _f_bound, f_support, f_mem⟩

Premises used: isOpen_interior, 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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
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 μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
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_support : Function.support f ⊆ interior k
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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
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 μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
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_support : Function.support f ⊆ interior k
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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
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 μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
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_support : Function.support f ⊆ interior k
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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
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_compact : IsCompact s
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 μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
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_support : Function.support f ⊆ interior k
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]