case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
⊢ ↑sign (prodCongrRight σ) = ∏ k : α, ↑sign (σ k)
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ↑sign (prodCongrRight σ) = ∏ k : α, ↑sign (σ k)
obtain ⟨l, hl, mem_l⟩ := Finite.exists_univ_list α
case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
l_to_finset : List.toFinset l = univ
⊢ ↑sign (prodCongrRight σ) = ∏ k : α, ↑sign (σ k)
case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
⊢ ↑sign (prodCongrRight σ) = ∏ k : α, ↑sign (σ k)
have l_to_finset : l.toFinset = Finset.univ := by
  apply eq_top_iff.mpr
  intro b _
  exact List.mem_toFinset.mpr (mem_l b)
case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
l_to_finset : List.toFinset l = univ
⊢ List.prod (List.map (↑sign ∘ fun a => prodExtendRight a (σ a)) l) = List.prod (List.map (fun k => ↑sign (σ k)) l)
case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
l_to_finset : List.toFinset l = univ
⊢ ↑sign (prodCongrRight σ) = ∏ k : α, ↑sign (σ k)
rw [← prod_prodExtendRight σ hl mem_l, sign.map_list_prod, List.map_map, ← l_to_finset,
  List.prod_toFinset _ hl]
no goals
case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
l_to_finset : List.toFinset l = univ
⊢ List.prod (List.map (↑sign ∘ fun a => prodExtendRight a (σ a)) l) = List.prod (List.map (fun k => ↑sign (σ k)) l)
simp_rw [← fun a => sign_prodExtendRight a (σ a), Function.comp]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
⊢ ⊤ ≤ List.toFinset l
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
⊢ List.toFinset l = univ
apply eq_top_iff.mpr
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
b : α
a✝ : b ∈ ⊤
⊢ b ∈ List.toFinset l
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
⊢ ⊤ ≤ List.toFinset l
intro b _
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
b : α
a✝ : b ∈ ⊤
⊢ b ∈ List.toFinset l
exact List.mem_toFinset.mpr (mem_l b)