awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
⊢ 0 < ε'

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
⊢ 0 < ε'

Tactic:
have hε' : 0 < ε' := by positivity
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
rw :
  ENNReal.ofReal ε' * ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))) ^ (1 / p.toReal) ≤
    ENNReal.ofReal ε
rw₁ :
  ENNReal.ofReal ε' * ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (1 / p.toReal)) ≤
    ENNReal.ofReal ε
rw₂ : ENNReal.ofReal (ε' * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (1 / p.toReal)) ≤ ENNReal.ofReal ε
rw₃ : ε' * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (1 / p.toReal) ≤ ε
rw₄ :
  ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal)) *
      ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (1 / p.toReal) ≤
    ε
rw₅ :
  ε *
      (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal)) *
        ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (1 / p.toReal)) ≤
    ε
rw₆ : ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal) + 1 / p.toReal) ≤ ε
rw₇ : ε * HPow.hPow (β := ℝ) (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))) 0 ≤ ε
rw₈ : ε * 1 ≤ ε
rw₉ rw₁₀ : ε ≤ ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε

Tactic:
rw [← ofReal_toReal hs₁, ofReal_rpow_of_pos hs₂, ← ofReal_mul hε'.le,
      ofReal_le_ofReal_iff hε.le, ε'_def, mul_assoc, ← Real.rpow_add hs₂, neg_add_cancel,
      Real.rpow_zero, mul_one]

Premises used: ENNReal.ofReal_rpow_of_pos, ENNReal.ofReal_le_ofReal_iff, ENNReal.ofReal_mul, mul_assoc, Real.rpow_zero, ENNReal.ofReal_toReal, LT.lt.le, neg_add_cancel, Real.rpow_add, mul_one
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε

Tactic:
have hε₂ : ENNReal.ofReal ε' * μ (tsupport f) ^ (1 / p.toReal) ≤ ENNReal.ofReal ε := by
    rw [← ofReal_toReal hs₁, ofReal_rpow_of_pos hs₂, ← ofReal_mul hε'.le,
      ofReal_le_ofReal_iff hε.le, ε'_def, mul_assoc, ← Real.rpow_add hs₂, neg_add_cancel,
      Real.rpow_zero, mul_one]
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ :
  ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
⊢ Continuous (Y := ℝ) fun (x : E) ↦ ε'

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ :
  ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
x : E
⊢ LT.lt (α := ℝ) 0 ((fun (x : E) ↦ ε') x)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ :
  ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
neg :
  ∀ (g : E → F) (hg₁ : ContDiff ℝ ∞ g) (hg₂ : ∀ (x : E), dist (g x) (f x) < ε')
    (hg₃ : Function.support g ⊆ Function.support f),
    ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨g, hg₁, hg₂, hg₃⟩ := h₂.exists_contDiff_approx ⊤ (ε := fun _ ↦ ε') (by fun_prop)
    (by intro; positivity)

Premises used: Continuous.exists_contDiff_approx, Top.top
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ :
  ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε'
hg₃ : Function.support g ⊆ Function.support f
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
⟨g, h₁.mono hg₃, hg₁, (eLpNorm_sub_le_of_dist_bdd μ hp h₁.measurableSet hε'.le ?_
    (subset_tsupport f) (hg₃.trans (subset_tsupport f))).trans hε₂⟩

Premises used: subset_tsupport, HasSubset.Subset.trans, LT.lt.le, HasCompactSupport.mono, And.intro, Exists.intro, LE.le.trans, MeasureTheory.eLpNorm_sub_le_of_dist_bdd, IsCompact.measurableSet
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ :
  ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε'
hg₃ : Function.support g ⊆ Function.support f
neg : ∀ (x : E), dist (f x) (g x) ≤ ε'
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨g, h₁.mono hg₃, hg₁, (eLpNorm_sub_le_of_dist_bdd μ hp h₁.measurableSet hε'.le ?_
    (subset_tsupport f) (hg₃.trans (subset_tsupport f))).trans hε₂⟩
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ :
  ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε'
hg₃ : Function.support g ⊆ Function.support f
x : E
neg : dist (g x) (f x) ≤ ε'
⊢ dist (f x) (g x) ≤ ε'

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ :
  ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε'
hg₃ : Function.support g ⊆ Function.support f
x : E
⊢ dist (g x) (f x) ≤ ε'

Tactic:
(hg₂ x).le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
ε' : ℝ := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
ε'_def : ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ :
  ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε'
hg₃ : Function.support g ⊆ Function.support f
x : E
⊢ dist (g x) (f x) ≤ ε'

Tactic:
exact (hg₂ x).le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
⊢ 0 < ε / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
⊢ 0 < ε / 2

Tactic:
have hε₂ : 0 < ε / 2 := by positivity
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
⊢ 0 < ENNReal.ofReal (ε / 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
⊢ 0 < ENNReal.ofReal (ε / 2)

Tactic:
have hε₂' : 0 < ENNReal.ofReal (ε / 2) := by positivity
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
obtain :
  ∀ (g : E → F) (hg₁ : HasCompactSupport g) (hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)) (hg₃ : Continuous g)
    (hg₄ : MemLp g p μ), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨g, hg₁, hg₂, hg₃, hg₄⟩ := hf.exists_hasCompactSupport_eLpNorm_sub_le hp hε₂'.ne'

Premises used: MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le, LT.lt.ne'
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
obtain :
  ∀ (g' : E → F) (hg'₁ : HasCompactSupport g') (hg'₂ : ContDiff ℝ ∞ g')
    (hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)),
    ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨g', hg'₁, hg'₂, hg'₃⟩ := hg₁.exist_eLpNorm_sub_le_of_continuous μ hε₂ hg₃

Premises used: HasCompactSupport.exist_eLpNorm_sub_le_of_continuous
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
⟨g', hg'₁, hg'₂, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
refine : eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨g', hg'₁, hg'₂, ?_⟩
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
⊢ f - g' = f - g - (g' - g)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
⊢ f - g' = f - g - (g' - g)

Tactic:
have : f - g' = (f - g) - (g' - g) := by simp
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') p μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
grw : eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
grw₁ : eLpNorm (f - g) p μ + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₂ : ENNReal.ofReal (ε / 2) + eLpNorm (g' - g) p μ ≤ ENNReal.ofReal ε
grw₃ : ENNReal.ofReal (ε / 2) + eLpNorm (g - g') p μ ≤ ENNReal.ofReal ε
grw₄ : ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
grw₅ : ENNReal.ofReal (ε / 2 + ε / 2) ≤ ENNReal.ofReal ε
grw₆ grw₇ : ENNReal.ofReal ε ≤ ENNReal.ofReal ε
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε

Tactic:
grw [this, eLpNorm_sub_le (hf.aestronglyMeasurable.sub hg₄.aestronglyMeasurable)
    (hg'₂.continuous.aestronglyMeasurable.sub hg₄.aestronglyMeasurable) hp₂, hg₂,
    eLpNorm_sub_comm, hg'₃, ← ENNReal.ofReal_add hε₂.le hε₂.le, add_halves]

Premises used: add_halves, MeasureTheory.eLpNorm_sub_le, MeasureTheory.AEStronglyMeasurable.sub, ContDiff.continuous, MeasureTheory.eLpNorm_sub_comm, LT.lt.le, ENNReal.ofReal_add, MeasureTheory.MemLp.aestronglyMeasurable, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Normed.Lp.SmoothApprox
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
⊢ Membership.mem (γ := Set ↥(Lp F p μ))
    (closure
      {f : ↥(Lp F p μ) | ∃ (g : E → F), (↑(↑f : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g})
    f

Tactic:
(mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_

Premises used: Iff.mpr, Metric.nhds_basis_closedBall, mem_closure_iff_nhds_basis