no goals
E : Type u_1
X : Type ?u.1158619
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
f : ContDiffBump 0
x : E
⊢ ContDiffBump.normed f μ (-x) = ContDiffBump.normed f μ x
simp_rw [f.normed_def, f.neg]