rcases hf.2 n with ⟨k_f, C_f, hC_f⟩
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k