have hf0 : (1 + ‖f x‖) ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
case hf0
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0

case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)