awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
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))
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have ε'_def : let ε' := ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal));
ε' = ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal))
Tactic: set ε' := ε * (μ <| tsupport f).toReal ^ (-(1 / p.toReal)) with ε'_def
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
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))
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have hε' : 0 < ε'
Tactic: have hε' : 0 < ε' := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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 ε
have rw : ENNReal.ofReal ε' * ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))) ^ (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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 ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
have rw₁ : ENNReal.ofReal ε' * ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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 ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
have rw₂ : ENNReal.ofReal (ε' * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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 ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
have rw₃ : ε' * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (1 / p.toReal) ≤ ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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) ≤
    ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
have rw₅ : ε *
    (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal)) *
      ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (1 / p.toReal)) ≤
  ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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)) ≤
    ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
have rw₆ : ε * ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f)) ^ (-(1 / p.toReal) + 1 / p.toReal) ≤ ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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) ≤ ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
have rw₇ : ε * HPow.hPow (β := ℝ) (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))) 0 ≤ ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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 ≤ ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
have rw₈ : ε * 1 ≤ ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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 ≤ ε
⊢ ENNReal.ofReal ε' * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal ε
have rw₉ : ε ≤ ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
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 < ε'
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have hε₂ : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have 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 ε
Tactic: obtain ⟨g, hg₁, hg₂, hg₃⟩ := h₂.exists_contDiff_approx ⊤ (ε := fun _ ↦ ε') (by fun_prop)
    (by intro; positivity)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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 ε
have neg : ∀ (x : E), dist (f x) (g x) ≤ ε'
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ε₂⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
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 (f x) (g x) ≤ ε'
have neg : dist (g x) (f x) ≤ ε'
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
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 < ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have hε₂ : 0 < ε / 2
Tactic: have hε₂ : 0 < ε / 2 := by positivity