no goals
α : Type u_3
β : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
ι : Type u_2
s : Finset ι
f : ι → C(α, β)
a : α
⊢ ↑(∏ i in s, f i) a = ∏ i in s, ↑(f i) a
simp