∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace ℝ G]
  [CompleteSpace E'] [BorelSpace G] [inst_7 : FiniteDimensional ℝ G] [μ.IsAddHaarMeasure] {ι : Type u_1}
  {φ : ι → ContDiffBump 0} {l : Filter ι} {K : ℝ},
  Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
    (∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn) →
      MeasureTheory.LocallyIntegrable g μ →
        ∀ᵐ (x₀ : G) ∂μ,
          Filter.Tendsto (fun i => MeasureTheory.convolution ((φ i).normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) l
            (nhds (g x₀))