α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ∀ (x : β × α), ↑(prodComm β α) (↑(prodCongrLeft σ) x) = ↑(prodCongrRight σ) (↑(prodComm β α) x)
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ↑sign (prodCongrLeft σ) = ∏ k : α, ↑sign (σ k)
refine' (sign_eq_sign_of_equiv _ _ (prodComm β α) _).trans (sign_prodCongrRight σ)
case mk
α✝ : Type u
β : Type v
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α✝ → Perm β
b : β
α : α✝
⊢ ↑(prodComm β α✝) (↑(prodCongrLeft σ) (b, α)) = ↑(prodCongrRight σ) (↑(prodComm β α✝) (b, α))
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ∀ (x : β × α), ↑(prodComm β α) (↑(prodCongrLeft σ) x) = ↑(prodCongrRight σ) (↑(prodComm β α) x)
rintro ⟨b, α⟩
no goals
case mk
α✝ : Type u
β : Type v
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α✝ → Perm β
b : β
α : α✝
⊢ ↑(prodComm β α✝) (↑(prodCongrLeft σ) (b, α)) = ↑(prodCongrRight σ) (↑(prodComm β α✝) (b, α))
rfl