no goals
E : Type u_1
X : Type ?u.2093391
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 μ
⊢ tsupport (ContDiffBump.normed f μ) = closedBall c f.rOut
rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']