. refine le_trans (hC_f x) ?_
  refine mul_le_mul_of_nonneg_left ?_ hC_f_nonneg
  exact pow_le_pow_right (by simp) (by simp)
case h.refine_1
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_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ max k_f k_g

case h.refine_2
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_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ max k_f k_g
case h.refine_2
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_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ max k_f k_g