. refine Continuous.aestronglyMeasurable ?_
  exact Continuous.sub hφ.continuous continuous_const
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume

case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C