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 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have obtain : ∀ (s : Set α) (st : s ⊆ t) (s_compact : IsCompact s) (s_closed : IsClosed[inst] s)
  (μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)),
  ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
Tactic: obtain ⟨s, st, s_compact, s_closed, μs⟩ :
      ∃ s, s ⊆ t ∧ IsCompact s ∧ IsClosed s ∧ μ (t \ s) < η :=
    ht.exists_isCompact_isClosed_diff_lt htμ.ne hη_pos'.ne'
-- 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 μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hsμ : μ s < ∞ := (measure_mono st).trans_lt htμ
-- 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 μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
have rw : eLpNorm.{u_1, u_2} (ε := E) ((t \ s).indicator fun (_y : α) ↦ c) p μ ≤ δ
Tactic: rw [← eLpNorm_neg, neg_sub, ← indicator_diff st]
-- 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 μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
Tactic: have I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ := by
    rw [← eLpNorm_neg, neg_sub, ← indicator_diff st]
    exact hη _ μs.le
-- 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 μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have obtain : ∀ (k : Set α) (k_compact : IsCompact k) (sk : s ⊆ interior k),
  ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
Tactic: obtain ⟨k, k_compact, sk⟩ : ∃ k : Set α, IsCompact k ∧ s ⊆ interior k :=
    exists_compact_superset s_compact
-- 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 μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have rcases : ∀ (f : α → E) (f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f)
  (I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ)
  (_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖) (f_support : Function.support f ⊆ interior k) (f_mem : MemLp f p μ),
  ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
Tactic: rcases exists_continuous_eLpNorm_sub_le_of_closed hp s_closed isOpen_interior sk hsμ.ne c δpos.ne'
    with ⟨f, f_cont, I2, _f_bound, f_support, f_mem⟩
-- 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_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : MemLp f p μ
⊢ eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
have h : (f - t.indicator fun (_y : α) ↦ c) =
  (f - s.indicator fun (x : α) ↦ c) + HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
Tactic: convert!
      (hδ _ _
          (f_mem.aestronglyMeasurable.sub
            (aestronglyMeasurable_const.indicator s_closed.measurableSet))
          ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub
            (aestronglyMeasurable_const.indicator ht))
          I2 I1).le using 2
-- 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_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : MemLp f p μ
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
Tactic: have I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε := by
    convert!
      (hδ _ _
          (f_mem.aestronglyMeasurable.sub
            (aestronglyMeasurable_const.indicator s_closed.measurableSet))
          ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub
            (aestronglyMeasurable_const.indicator ht))
          I2 I1).le using 2
    simp only [sub_add_sub_cancel]
-- 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_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : MemLp f p μ
I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
⊢ ∃ (g : α → E),
    eLpNorm (g - t.indicator fun (x : α) ↦ c) p μ ≤ ε ∧
      Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
have refine : ∀ (x : α) (hx : x ∉ k), f x = 0
Tactic: refine ⟨f, I3, f_cont, f_mem, HasCompactSupport.intro k_compact fun x hx => ?_⟩
-- 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_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : MemLp f p μ
I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
x : α
hx : x ∉ k
⊢ f x = 0
have rw : x ∉ Function.support f
Tactic: rw [← Function.notMem_support]
-- 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_1 : α → E
hf : MemLp f_1 p μ
ε_1 : ℝ≥0∞
hε_1 : ε_1 ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη :
  ∀ (s : Set α),
    (μ : (a : Set α) → ℝ≥0∞) s ≤ (↑η : ℝ≥0∞) → eLpNorm.{u_1, u_2} (ε := E) (s.indicator fun (_x : α) ↦ c) p μ ≤ δ
hη_pos' : 0 < (↑η : ℝ≥0∞)
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst] s
μs : (μ : (a : Set α) → ℝ≥0∞) (t \ s) < (↑η : ℝ≥0∞)
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
I1 : eLpNorm (HSub.hSub (α := (x : α) → E) (s.indicator fun (_y : α) ↦ c) (t.indicator fun (_y : α) ↦ c)) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm.{u_1, u_2} (ε := E) (fun (x : α) ↦ f x - s.indicator (fun (_y : α) ↦ c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : MemLp f p μ
I3 : eLpNorm (f - t.indicator fun (_y : α) ↦ c) p μ ≤ ε
x : α
hx : x ∉ k
⊢ x ∉ Function.support f
have contrapose : ∀ (hx : x ∈ Function.support f), x ∈ k
Tactic: contrapose hx
Cleared hypotheses: 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 α
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal p) μ
have I : 0 < ε ^ (1 / p)
Tactic: have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _
-- 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 α
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal p) μ
have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
Tactic: have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0 := by
    simp only [Ne, ENNReal.ofReal_eq_zero, not_le, I]
-- 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 α
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal p) μ
have B : ENNReal.ofReal p ≠ 0
Tactic: have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne, ENNReal.ofReal_eq_zero, not_le] using hp
-- 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 α
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal p) μ
have rcases : ∀ (g : α → E) (g_support : HasCompactSupport g)
  (hg : eLpNorm (f - g) (↑p.toNNReal : ℝ≥0∞) μ ≤ ENNReal.ofReal (ε ^ (1 / p)))
  (g_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g)
  (g_mem : MemLp g (↑p.toNNReal : ℝ≥0∞) μ),
  ∃ (g : α → E),
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal p) μ
Tactic: rcases hf.exists_hasCompactSupport_eLpNorm_sub_le ENNReal.coe_ne_top A with
    ⟨g, g_support, hg, g_cont, g_mem⟩
-- 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 α
inst_5 : NormedSpace ℝ E
inst_6 : R1Space α
inst_7 : WeaklyLocallyCompactSpace α
inst_8 : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
hg : eLpNorm (f - g) (↑p.toNNReal : ℝ≥0∞) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
g_cont : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g (↑p.toNNReal : ℝ≥0∞) μ
⊢ ∃ (g : α → E),
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧
        Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal p) μ
have hg₁ : eLpNorm (f - g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
Tactic: change eLpNorm _ (ENNReal.ofReal p) _ ≤ _ at hg
Cleared hypotheses: hg