α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
l : List α
hl : Quotient.mk (List.isSetoid α) l = s
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
let ⟨l, hl⟩ := Quotient.exists_rep s
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
l : List α
hl : Quotient.mk (List.isSetoid α) l = s
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
l : List α
hl : Quotient.mk (List.isSetoid α) l = s
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
let e := equivFin α
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
l : List α
hl : Quotient.mk (List.isSetoid α) l = s
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
subst hl
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
show
  signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ ∀ x y, x ≠ y → signAux2 l (swap x y) = -1
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e :=
  Equiv.ext fun h => by simp [mul_apply]
case left
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g

case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
constructor
no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
h : Fin (Fintype.card α)
⊢ ↑((e.symm.trans (f * g)).trans e) h = ↑((e.symm.trans f).trans e * (e.symm.trans g).trans e) h
simp [mul_apply]
no goals
case left
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
  signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
  hfg, signAux_mul]
case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : x ≠ y
⊢ signAux2 l (swap x y) = -1
case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
intro x y hxy
case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : x ≠ y
hexy : ↑e x ≠ ↑e y
⊢ signAux2 l (swap x y) = -1
case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : x ≠ y
⊢ signAux2 l (swap x y) = -1
have hexy : e x ≠ e y := mt e.injective.eq_iff.1 hxy
no goals
case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : x ≠ y
hexy : ↑e x ≠ ↑e y
⊢ signAux2 l (swap x y) = -1
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hexy]