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 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
g : C(α, ℝ)
hgv : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 0 (u ∩ V)ᶜ
hgs : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 1 s
hg_range : ∀ (x : α), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : α) → ℝ) x : ℝ)
g_norm : ∀ (x : α), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x
gc_bd0 : ∀ (x : α), ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c‖ ≤ ‖c‖
gc_bd :
  ∀ (x : α),
    ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
      norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
gc_support : (Function.support.{u_1, u_2} (M := E) fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) ⊆ v
⊢ MemLp.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) p μ

Tactic:
have gc_mem : MemLp (fun x => g x • c) p μ := by
    refine MemLp.smul (memLp_top_const _) ?_ (p := p) (q := ∞)
    refine ⟨g.continuous.aestronglyMeasurable, ?_⟩
    have : eLpNorm (v.indicator fun _x => (1 : ℝ)) p μ < ⊤ :=
      (eLpNorm_indicator_const_le _ _).trans_lt <| by simp [lt_top_iff_ne_top, hμv.ne]
    refine (eLpNorm_mono fun x => ?_).trans_lt this
    by_cases hx : x ∈ v
    · simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs,
        indicator_of_mem, CStarRing.norm_one]
    · simp only [hgv hx, Pi.zero_apply, Real.norm_eq_abs, abs_zero, abs_nonneg]
-- 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 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
g : C(α, ℝ)
hgv : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 0 (u ∩ V)ᶜ
hgs : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 1 s
hg_range : ∀ (x : α), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : α) → ℝ) x : ℝ)
g_norm : ∀ (x : α), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x
gc_bd0 : ∀ (x : α), ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c‖ ≤ ‖c‖
gc_bd :
  ∀ (x : α),
    ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
      norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
gc_support : (Function.support.{u_1, u_2} (M := E) fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) ⊆ v
gc_mem : MemLp.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) p μ
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : α) ↦
    HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c

Tactic:
fun_prop
-- 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 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
g : C(α, ℝ)
hgv : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 0 (u ∩ V)ᶜ
hgs : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 1 s
hg_range : ∀ (x : α), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : α) → ℝ) x : ℝ)
g_norm : ∀ (x : α), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x
gc_bd0 : ∀ (x : α), ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c‖ ≤ ‖c‖
gc_bd :
  ∀ (x : α),
    ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
      norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
gc_support : (Function.support.{u_1, u_2} (M := E) fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) ⊆ v
gc_mem : MemLp.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) p μ
refine : eLpNorm.{u_1, u_2} (ε := E) ((v \ s).indicator fun (_x : α) ↦ c) p μ ≤ ε
⊢ ∃ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ

Tactic:
refine ⟨fun x ↦ g x • c, by fun_prop, (eLpNorm_mono gc_bd).trans ?_, gc_bd0,
      gc_support.trans inter_subset_left, gc_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 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
g : C(α, ℝ)
hgv : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 0 (u ∩ V)ᶜ
hgs : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 1 s
hg_range : ∀ (x : α), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : α) → ℝ) x : ℝ)
g_norm : ∀ (x : α), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x
gc_bd0 : ∀ (x : α), ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c‖ ≤ ‖c‖
gc_bd :
  ∀ (x : α),
    ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
      norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
gc_support : (Function.support.{u_1, u_2} (M := E) fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) ⊆ v
gc_mem : MemLp.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) p μ
⊢ eLpNorm.{u_1, u_2} (ε := E) ((v \ s).indicator fun (_x : α) ↦ c) p μ ≤ ε

Tactic:
hη _ ((measure_mono (diff_subset_diff inter_subset_right Subset.rfl)).trans hV.le)

Premises used: Set.diff_subset_diff, LT.lt.le, Set.Subset.rfl, MeasureTheory.measure_mono, LE.le.trans, Set.inter_subset_right
-- 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 : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst] s
u_open : IsOpen[inst] u
hsu : s ⊆ u
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ ε
ηpos : 0 < (↑η : ℝ≥0∞)
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst] V
h'V : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hV : (μ : (a : Set α) → ℝ≥0∞) (V \ s) < (↑η : ℝ≥0∞)
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
g : C(α, ℝ)
hgv : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 0 (u ∩ V)ᶜ
hgs : EqOn (β := ℝ) (⇑g : (a : α) → ℝ) 1 s
hg_range : ∀ (x : α), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g : (a : α) → ℝ) x : ℝ)
g_norm : ∀ (x : α), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x
gc_bd0 : ∀ (x : α), ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c‖ ≤ ‖c‖
gc_bd :
  ∀ (x : α),
    ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
      norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
gc_support : (Function.support.{u_1, u_2} (M := E) fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) ⊆ v
gc_mem : MemLp.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) p μ
⊢ eLpNorm.{u_1, u_2} (ε := E) ((v \ s).indicator fun (_x : α) ↦ c) p μ ≤ ε

Tactic:
exact hη _ ((measure_mono (diff_subset_diff inter_subset_right Subset.rfl)).trans hV.le)

Premises used: Set.diff_subset_diff, LT.lt.le, Set.Subset.rfl, MeasureTheory.measure_mono, LE.le.trans, Set.inter_subset_right
-- 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 μ
ε : ℝ≥0∞
hε : ε ≠ 0
H :
  ∃ (g : α → E),
    eLpNorm (f - g) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
rcases :
  ∀ (g : α → E) (hg : eLpNorm (f - g) p μ ≤ ε)
    (g_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g) (g_mem : MemLp g p μ)
    (g_support : HasCompactSupport g),
    ∃ (g : α → E),
      HasCompactSupport g ∧
        eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ

Tactic:
rcases H with ⟨g, hg, g_cont, g_mem, g_support⟩
-- 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 μ
ε : ℝ≥0∞
hε : ε ≠ 0
g : α → E
hg : eLpNorm (f - g) p μ ≤ ε
g_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g p μ
g_support : HasCompactSupport g
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ

Tactic:
⟨g, g_support, hg, g_cont, 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 α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
g : α → E
hg : eLpNorm (f - g) p μ ≤ ε
g_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g p μ
g_support : HasCompactSupport g
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ

Tactic:
exact ⟨g, g_support, hg, g_cont, 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 α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
suffices :
  ∃ (g : α → E),
    eLpNorm (f - g) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ

Tactic:
suffices H :
      ∃ g : α → E, eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ ∧ HasCompactSupport g by
    rcases H with ⟨g, hg, g_cont, g_mem, g_support⟩
    exact ⟨g, g_support, hg, g_cont, 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 α
p : ℝ≥0∞
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
apply :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ {ε : ℝ≥0∞},
          ε ≠ 0 →
            ∃ (g : α → E),
              eLpNorm (g - s.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
                Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧
                  MemLp g p μ ∧ HasCompactSupport g
apply₁ :
  ∀ (f g : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ MemLp f p μ ∧ HasCompactSupport f →
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g →
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f + g) ∧
          MemLp (f + g) p μ ∧ HasCompactSupport (f + g)
apply₂ :
  ∀ (f : α → E),
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ MemLp f p μ ∧ HasCompactSupport f →
      AEStronglyMeasurable f μ
⊢ ∃ (g : α → E),
    eLpNorm (f - g) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g

Tactic:
apply hf.induction_dense hp _ _ _ _ hε

Premises used: MeasureTheory.MemLp.induction_dense
-- 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_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
f_mem : MemLp f p μ
hf : HasCompactSupport f
g_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g p μ
hg : HasCompactSupport g
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f + g) ∧
    MemLp (f + g) p μ ∧ HasCompactSupport (f + g)

Tactic:
⟨f_cont.add g_cont, f_mem.add g_mem, hf.add hg⟩

Premises used: MeasureTheory.MemLp.add, HasCompactSupport.add, And.intro, Continuous.add
-- 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_1 : MemLp f_1 p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
f_mem : MemLp f p μ
hf : HasCompactSupport f
g_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g p μ
hg : HasCompactSupport g
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f + g) ∧
    MemLp (f + g) p μ ∧ HasCompactSupport (f + g)

Tactic:
exact ⟨f_cont.add g_cont, f_mem.add g_mem, hf.add hg⟩
-- 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 μ
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → E
_f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
f_mem : MemLp f p μ
_hf : HasCompactSupport f
⊢ AEStronglyMeasurable f μ

Tactic:
f_mem.aestronglyMeasurable

Premises used: 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 μ
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → E
_f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
f_mem : MemLp f p μ
_hf : HasCompactSupport f
⊢ AEStronglyMeasurable f μ

Tactic:
exact f_mem.aestronglyMeasurable

Premises used: 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 : α → 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
rcases :
  ∀ (δ : ℝ≥0∞) (δpos : 0 < δ)
    (hδ :
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) 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_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩

Premises used: MeasureTheory.exists_Lp_half
-- 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),
    0 < η ∧
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ

Tactic:
exists_eLpNorm_indicator_le hp c δpos.ne'

Premises used: LT.lt.ne', MeasureTheory.exists_eLpNorm_indicator_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 μ < ε
obtain :
  ∀ (η : ℝ≥0) (ηpos : 0 < η)
    (hη :
      ∀ (s : Set α),
        (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) 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:
obtain ⟨η, ηpos, hη⟩ :
      ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ :=
    exists_eLpNorm_indicator_le hp c δpos.ne'

Premises used: LT.lt.ne', MeasureTheory.exists_eLpNorm_indicator_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 μ ≤ δ
⊢ 0 < (↑η : ℝ≥0∞)

Tactic:
have hη_pos' : (0 : ℝ≥0∞) < η := ENNReal.coe_pos.2 ηpos