refine ⟨contDiff_id, ?_⟩
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
⊢ HasTemperateGrowth id
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n id x‖ ≤ C * (1 + ‖x‖) ^ k