awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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 μ
have refine : eLpNorm (ε := ℝ) (⇑g : (a : α) → ℝ) p μ < ∞
Tactic: refine ⟨g.continuous.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
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 (ε := ℝ) (⇑g : (a : α) → ℝ) p μ < ∞
have this : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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 μ < ∞
have refine : ∀ (x : α), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)
Tactic: refine (eLpNorm_mono fun x => ?_).trans_lt this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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 : α
⊢ norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)
have pos : ∀ (hx : x ∈ v), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)
Tactic: by_cases hx : x ∈ v
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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)
⊢ norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)
have neg : ∀ (hx : x ∉ v), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) ≤ norm (E := ℝ) (v.indicator (fun (_x : α) ↦ 1) x)
Tactic: by_cases hx : x ∈ v
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
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
⊢ ∃ (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 μ
have gc_mem : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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 μ
⊢ ∃ (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 μ
have refine : eLpNorm.{u_1, u_2} (ε := E) ((v \ s).indicator fun (_x : α) ↦ c) 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ
have 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 μ
Tactic: rcases H with ⟨g, hg, g_cont, g_mem, g_support⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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),
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ
have suffices : ∃ (g : α → E),
  eLpNorm (f - g) p μ ≤ ε ∧
    Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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),
    eLpNorm (f - g) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have 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
Tactic: apply hf.induction_dense hp _ _ _ _ hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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
⊢ ∃ (g : α → E),
    eLpNorm (f - g) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have 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)
Tactic: apply hf.induction_dense hp _ _ _ _ hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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)
⊢ ∃ (g : α → E),
    eLpNorm (f - g) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have apply₂ : ∀ (f : α → E),
  Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ MemLp f p μ ∧ HasCompactSupport f →
    AEStronglyMeasurable f μ
Tactic: apply hf.induction_dense hp _ _ _ _ hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have 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
Tactic: rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (goal)
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 μ < ε
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have 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
Tactic: obtain ⟨η, ηpos, hη⟩ :
      ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ :=
    exists_eLpNorm_indicator_le hp c δpos.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ContinuousMapDense (hypothesis)
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 μ ≤ δ
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have hη_pos' : 0 < (↑η : ℝ≥0∞)
Tactic: have hη_pos' : (0 : ℝ≥0∞) < η := ENNReal.coe_pos.2 ηpos