have h_neg {x : α} : -x = (Homeomorph.neg α) x := by simp [Homeomorph.neg]
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ HasCompactSupport fun x => f (-x)
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f (-x)