case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
⊢ signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s : Multiset α
t : Multiset β
hs : ∀ (x : α), x ∈ s
ht : ∀ (x : β), x ∈ t
⊢ signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs
induction' t, s using Quotient.inductionOn₂ with t s ht hs
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
⊢ signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs
show signAux2 _ _ = signAux2 _ _
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
n : β ≃ Fin (Fintype.card β) := Fintype.equivFin β
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f
let n := equivFin β
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
n : β ≃ Fin (Fintype.card β) := Fintype.equivFin β
⊢ signAux ((n.symm.trans ((e.symm.trans f).trans e)).trans n) = signAux (((e.trans n).symm.trans f).trans (e.trans n))
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
n : β ≃ Fin (Fintype.card β) := Fintype.equivFin β
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f
rw [← signAux_eq_signAux2 _ _ n fun _ _ => ht _,
  ← signAux_eq_signAux2 _ _ (e.trans n) fun _ _ => hs _]
no goals
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
n : β ≃ Fin (Fintype.card β) := Fintype.equivFin β
⊢ signAux ((n.symm.trans ((e.symm.trans f).trans e)).trans n) = signAux (((e.trans n).symm.trans f).trans (e.trans n))
exact congr_arg signAux
  (Equiv.ext fun x => by simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply])
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
n : β ≃ Fin (Fintype.card β) := Fintype.equivFin β
x : Fin (Fintype.card β)
⊢ ↑((n.symm.trans ((e.symm.trans f).trans e)).trans n) x = ↑(((e.trans n).symm.trans f).trans (e.trans n)) x
simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply]