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)
x : α
hx : x ∉ v
⊢ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c = 0

Tactic:
simp only [hgv hx, Pi.zero_apply, zero_smul]

Premises used: Pi.zero_apply, zero_smul
-- 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)
⊢ (Function.support.{u_1, u_2} (M := E) fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) ⊆ v

Tactic:
have gc_support : (Function.support fun x : α => g x • c) ⊆ v := by
    refine Function.support_subset_iff'.2 fun x hx => ?_
    simp only [hgv hx, Pi.zero_apply, zero_smul]
-- 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:
MemLp.smul (memLp_top_const _) ?_ (p := p) (q := ∞)

Premises used: MeasureTheory.MemLp.smul, MeasureTheory.memLp_top_const
-- 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
refine : MemLp (ε := ℝ) (⇑g : (a : α) → ℝ) p μ
⊢ MemLp.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) p μ

Tactic:
refine MemLp.smul (memLp_top_const _) ?_ (p := p) (q := ∞)

Premises used: MeasureTheory.MemLp.smul, MeasureTheory.memLp_top_const
-- 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 (ε := ℝ) (⇑g : (a : α) → ℝ) p μ

Tactic:
⟨g.continuous.aestronglyMeasurable, ?_⟩

Premises used: ContinuousMap.continuous, MeasureTheory.MemLp, And.intro, Continuous.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 : μ.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
refine : eLpNorm (ε := ℝ) (⇑g : (a : α) → ℝ) p μ < ∞
⊢ MemLp (ε := ℝ) (⇑g : (a : α) → ℝ) p μ

Tactic:
refine ⟨g.continuous.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 : μ.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
⊢ enorm (E := ℝ) 1 * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (1 / p.toReal) < ∞

Tactic:
simp [lt_top_iff_ne_top, hμv.ne]

Premises used: lt_top_iff_ne_top, 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 : μ.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
⊢ eLpNorm (ε := ℝ) (v.indicator fun (_x : α) ↦ 1) p μ < ∞

Tactic:
have : eLpNorm (v.indicator fun _x => (1 : ℝ)) p μ < ⊤ :=
      (eLpNorm_indicator_const_le _ _).trans_lt <| by simp [lt_top_iff_ne_top, hμv.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 : μ.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
this : eLpNorm (ε := ℝ) (v.indicator fun (_x : α) ↦ 1) p μ < ∞
⊢ eLpNorm (ε := ℝ) (⇑g : (a : α) → ℝ) p μ < ∞

Tactic:
(eLpNorm_mono fun x => ?_).trans_lt this

Premises used: MeasureTheory.eLpNorm_mono, LE.le.trans_lt
-- 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
this : eLpNorm (ε := ℝ) (v.indicator fun (_x : α) ↦ 1) p μ < ∞
refine : ∀ (x : α), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)
⊢ eLpNorm (ε := ℝ) (⇑g : (a : α) → ℝ) p μ < ∞

Tactic:
refine (eLpNorm_mono fun x => ?_).trans_lt this

Premises used: MeasureTheory.eLpNorm_mono, LE.le.trans_lt
-- 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
this : eLpNorm (ε := ℝ) (v.indicator fun (_x : α) ↦ 1) p μ < ∞
x : α
pos : ∀ (hx : x ∈ v), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)
neg : ∀ (hx : x ∉ v), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)
⊢ norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)

Tactic:
by_cases hx : x ∈ v
-- 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
this : eLpNorm (ε := ℝ) (v.indicator fun (_x : α) ↦ 1) p μ < ∞
x : α
hx : x ∈ v
⊢ norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)

Tactic:
simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs,
        indicator_of_mem, CStarRing.norm_one]

Premises used: Set.indicator_of_mem, And.right, And.left, abs_of_nonneg, CStarRing.norm_one, Real.norm_eq_abs
-- 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
this : eLpNorm (ε := ℝ) (v.indicator fun (_x : α) ↦ 1) p μ < ∞
x : α
hx : x ∉ v
⊢ norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)

Tactic:
simp only [hgv hx, Pi.zero_apply, Real.norm_eq_abs, abs_zero, abs_nonneg]

Premises used: Pi.zero_apply, abs_zero, abs_nonneg, Real.norm_eq_abs