no goals
α✝ : Type ?u.124202
β : Type ?u.124205
γ : Type ?u.124208
ι : Type u_2
inst✝² : SeminormedRing α✝
α : Type u_1
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ∏ i in s, ‖f i‖ = (fun a => ↑a) (∏ i in s, ‖f i‖₊)
simp [NNReal.coe_prod]