refine ENNReal.toReal_le_of_le_ofReal C.prop ?_
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‖₊
⊢ ENNReal.toReal (∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖) ≤ ↑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‖₊
⊢ ∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖ ≤ ENNReal.ofReal ↑C