case h.e'_3.h
ι : Type ?u.291257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → β
hs : {a | ↑σ a ≠ a} ⊆ ↑s
⊢ s = map (Equiv.toEmbedding σ) s
ι : Type ?u.291257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → β
hs : {a | ↑σ a ≠ a} ⊆ ↑s
⊢ ∏ x in s, f (↑σ x) = ∏ x in s, f x
convert (prod_map s σ.toEmbedding f).symm
no goals
case h.e'_3.h
ι : Type ?u.291257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
σ : Equiv.Perm α
s : Finset α
f : α → β
hs : {a | ↑σ a ≠ a} ⊆ ↑s
⊢ s = map (Equiv.toEmbedding σ) s
exact (map_perm hs).symm