Theorem: Finset.prod_congr_equiv (DividedPowers/PolynomialMap/Coeff.lean)

State before:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
s : Finset α
e : α ≃ β
⊢ s.prod f = (map e.toEmbedding s).prod (f ∘ ⇑e.symm)
Tactic:
simp only [Function.comp_apply, prod_map, Equiv.coe_toEmbedding, Equiv.symm_apply_apply]
State after:
no goals