simpa [Finset.prod_insert hi] using HasTemperateGrowth.mul hf.1 (IH hf.2)
case insert
ι : Type u_1
inst✝⁴ : DecidableEq ι
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → ℝ
i : ι
s : Finset ι
hi : i ∉ s
IH : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x => ∏ i in s, f i x
hf : HasTemperateGrowth (f i) ∧ ∀ a ∈ s, HasTemperateGrowth (f a)
⊢ HasTemperateGrowth fun x => ∏ i in insert i s, f i x
no goals