. refine AEStronglyMeasurable.smul ?_ f.continuous.aestronglyMeasurable
  refine (AEMeasurable.pow_const ?_ n).aestronglyMeasurable
  exact (continuous_const.add continuous_norm).aemeasurable
case refine_1
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ n • f x) volume

case refine_2
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
⊢ HasFiniteIntegral fun x => (1 + ‖x‖) ^ n • f x
case refine_2
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
⊢ HasFiniteIntegral fun x => (1 + ‖x‖) ^ n • f x