induction s using Finset.induction with
| empty => simp [hasTemperateGrowth_const]
| @insert i s hi IH =>
  simp only [Finset.mem_insert, forall_eq_or_imp] at hf
  simpa [Finset.prod_insert hi] using HasTemperateGrowth.mul hf.1 (IH hf.2)
ι : 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
s : Finset ι
f : ι → E → ℝ
hf : ∀ i ∈ s, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth fun x => ∏ i in s, f i x
no goals