no goals
E : Type u_1
X : Type ?u.89198
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
hx : x ∈ ball c f.rOut
⊢ ↑f x ≠ 0
rwa [← support_eq, mem_support] at hx