no goals
ι : Type ?u.378826
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : α → β
this : DecidableEq α
⊢ ∏ x in image Subtype.val (attach s), f x = ∏ x in s, f x
rw [attach_image_val]