α : Type u_2
β : Type u_1
γ : Type ?u.34497
δ : Type ?u.34500
inst✝ : CommMonoid α
p : Finset β
f : β → α
this : (fun i => Associates.mk (f i)) = Associates.mk ∘ f
⊢ ∏ i in p, Associates.mk (f i) = Associates.mk (∏ i in p, f i)
α : Type u_2
β : Type u_1
γ : Type ?u.34497
δ : Type ?u.34500
inst✝ : CommMonoid α
p : Finset β
f : β → α
⊢ ∏ i in p, Associates.mk (f i) = Associates.mk (∏ i in p, f i)
have : (fun i => Associates.mk (f i)) = Associates.mk ∘ f :=
  funext <| fun x => Function.comp_apply
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.34497
δ : Type ?u.34500
inst✝ : CommMonoid α
p : Finset β
f : β → α
this : (fun i => Associates.mk (f i)) = Associates.mk ∘ f
⊢ ∏ i in p, Associates.mk (f i) = Associates.mk (∏ i in p, f i)
rw [Finset.prod_eq_multiset_prod, this, ←Multiset.map_map, prod_mk, ←Finset.prod_eq_multiset_prod]