. rw [HasFiniteIntegral]
  rw [← snorm_one_eq_lintegral_nnnorm]
  refine lt_of_le_of_lt ?_ (snorm_nnreal_one_add_norm_rpow_smul_lt_top n f zero_lt_one)
  refine snorm_mono ?_
  intro x
  simp [norm_smul]
  refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg (f x))
  rw [abs_of_nonneg (by simp)]
  refine pow_le_pow_left ?_ ?_ _ <;> simp
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 => ‖x‖ ^ n • f x
no goals