no goals
E : Type u_1
X : Type ?u.87643
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
⊢ tsupport ↑f = closedBall c f.rOut
simp_rw [tsupport, f.support_eq, closure_ball _ f.rOut_pos.ne']