case h.e'_2.a.h.e'_2
ι : Type ?u.298556
β : 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✝ : α
a✝ : x✝ ∈ s
⊢ x✝ = ↑σ.symm (↑σ x✝)
ι : Type ?u.298556
β : 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 = ∏ x in s, f x (↑σ.symm x)
convert σ.prod_comp s (fun x => f x (σ.symm x)) hs
no goals
case h.e'_2.a.h.e'_2
ι : Type ?u.298556
β : 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✝ : α
a✝ : x✝ ∈ s
⊢ x✝ = ↑σ.symm (↑σ x✝)
rw [Equiv.symm_apply_apply]