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 ∘ ⇑e) = (map e.toEmbedding s).prod f
Tactic:
simp only [Function.comp_apply, prod_map, Equiv.coe_toEmbedding]
State after:
no goals