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 : ℝ)
x : α
rw : Eq (α := ℝ) (|(g : (a : α) → ℝ) x| : ℝ) ((g : (a : α) → ℝ) x : ℝ)
⊢ norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x
have rw₁ : Eq (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]
-- 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 : ℝ)
⊢ ∃ (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 g_norm : ∀ (x : α), norm (E := ℝ) ((g : (a : α) → ℝ) x : ℝ) = (g : (a : α) → ℝ) x
Tactic: have g_norm : ∀ x, ‖g x‖ = g x := fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]
-- 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
x : α
⊢ ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c‖ ≤ ‖c‖
have simp : HMul.hMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) ‖c‖ ≤ ‖c‖
Tactic: simp only [norm_smul, g_norm x]
-- 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
x : α
⊢ HMul.hMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) ‖c‖ ≤ ‖c‖
have apply : LE.le (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) (1 : ℝ)
Tactic: apply mul_le_of_le_one_left (norm_nonneg _)
-- 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
⊢ ∃ (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_bd0 : ∀ (x : α), ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c‖ ≤ ‖c‖
Tactic: have gc_bd0 : ∀ x, ‖g x • c‖ ≤ ‖c‖ := by
    intro x
    simp only [norm_smul, g_norm x]
    apply mul_le_of_le_one_left (norm_nonneg _)
    exact (hg_range x).2
-- 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‖
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)
have pos : ∀ (hv : x ∈ v),
  ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
    norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
Tactic: by_cases hv : 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‖
x : α
pos :
  ∀ (hv : x ∈ v),
    ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
      norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) 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)
have neg : ∀ (hv : x ∉ v),
  ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
    norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
Tactic: by_cases hv : 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‖
x : α
hv : x ∈ v
⊢ ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
    norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
have hv₁ : x ∈ v \ s ∪ s
Tactic: rw [← Set.diff_union_of_subset hsv] at hv
Cleared hypotheses: hv
-- 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‖
x : α
hv : x ∈ v \ s ∪ s
⊢ ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
    norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
have pos : ∀ (hsv : x ∈ v \ s),
  ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
    norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
Tactic: rcases hv with hsv | hs
Cleared hypotheses: hv
-- 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‖
x : α
hv : x ∈ v \ s ∪ s
pos :
  ∀ (hsv : x ∈ v \ s),
    ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
      norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) 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)
have pos₁ : ∀ (hs : x ∈ s),
  ‖HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c - s.indicator (fun (_x : α) ↦ c) x‖ ≤
    norm.{u_2} (E := E) ((v \ s).indicator (fun (_x : α) ↦ c) x)
Tactic: rcases hv with hsv | hs
Cleared hypotheses: hv
-- 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‖
⊢ ∃ (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_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)
Tactic: have gc_bd :
      ∀ x, ‖g x • c - s.indicator (fun _x => c) x‖ ≤ ‖(v \ s).indicator (fun _x => c) x‖ := by
    intro x
    by_cases hv : x ∈ v
    · rw [← Set.diff_union_of_subset hsv] at hv
      rcases hv with hsv | hs
      · simpa only [hsv.2, Set.indicator_of_notMem, not_false_iff, sub_zero, hsv,
          Set.indicator_of_mem] using gc_bd0 x
      · simp [hgs hs, hs]
    · simp [hgv hv, show x ∉ s from fun h => hv (hsv 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 : μ.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
have refine : ∀ (x : α) (hx : x ∉ v), HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c = 0
Tactic: refine Function.support_subset_iff'.2 fun x hx => ?_
-- 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)
⊢ ∃ (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_support : (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]
-- 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.{u_1, u_2} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) ((g : (a : α) → ℝ) x : ℝ) c) p μ
have refine : MemLp (ε := ℝ) (⇑g : (a : α) → ℝ) p μ
Tactic: refine MemLp.smul (memLp_top_const _) ?_ (p := p) (q := ∞)