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