no goals
E : Type u_1
X : Type ?u.2210912
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
⊢ HasCompactSupport (ContDiffBump.normed f μ)
simp only [HasCompactSupport, f.tsupport_normed_eq (μ := μ), isCompact_closedBall]