∀ {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  [inst_6 : NormedSpace ℝ F] (μ : autoParam (MeasureTheory.Measure E) _auto_10✝)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] {p : ENNReal},
  p ≠ ⊤ →
    ∀ {ε : ℝ},
      0 < ε →
        ∀ {f : E → F},
          HasCompactSupport f →
            Continuous f →
              ∃ g, HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε