no goals
E : Type u_1
X : Type ?u.78048
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f✝ : ContDiffBump c
x✝ : E
n : ℕ∞
f : ContDiffBump 0
x : E
⊢ ↑f (-x) = ↑f x
simp_rw [← zero_sub, f.sub, zero_add]