simp [mul_assoc]
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∑ i in Finset.range (n + 1), ↑(Nat.choose n i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖ ≤
    ↑(2 ^ n) * C_f * C_g * (1 + ‖x‖) ^ (k_f + k_g)
case h
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
⊢ ∑ x_1 in Finset.range (n + 1), ↑(Nat.choose n x_1) * (‖iteratedFDeriv ℝ x_1 f x‖ * ‖iteratedFDeriv ℝ (n - x_1) g x‖) ≤
    2 ^ n * (C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g)))