rw [HasFiniteIntegral, lt_top_iff_ne_top, WithTop.ne_top_iff_exists] at this
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
this : HasFiniteIntegral fun x => g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
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
this : ∃ a, ↑a = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C