refine le_trans (lintegral_ofReal_le_lintegral_nnnorm _) ?_
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖ ≤ ENNReal.ofReal ↑C
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∫⁻ (x : ℝ), ↑‖‖g x‖‖₊ ≤ ENNReal.ofReal ↑C