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

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)