α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
this : f = 1
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have : f = 1 := Equiv.ext fun y => Classical.not_not.1 (mt (h y) (List.not_mem_nil _))
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
this : f = 1
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
⊢ signAux ((e.symm.trans f).trans e) = signAux2 (x :: l) f
rw [signAux2]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)

case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
by_cases hfx : x = f x
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = signAux2 l f
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
rw [if_pos hfx]
no goals
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = signAux2 l f
exact
  signAux_eq_signAux2 l f _ fun y (hy : f y ≠ y) =>
    List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h y hy)
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h✝ : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
y : α
hy : ↑f y ≠ y
h : y = x
⊢ False
simp [h, hfx.symm] at hy
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l := fun y hy =>
  have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
  List.mem_of_ne_of_mem this.2 (h _ this.1)
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
have : (e.symm.trans (swap x (f x) * f)).trans e =
    swap (e x) (e (f x)) * (e.symm.trans f).trans e := by
  ext
  rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
  repeat (rw [trans_apply])
  simp [swap, swapCore]
  split_ifs <;> rfl
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
hefx : ↑e x ≠ ↑e (↑f x)
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
have hefx : e x ≠ e (f x) := mt e.injective.eq_iff.1 hfx
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
hefx : ↑e x ≠ ↑e (↑f x)
⊢ signAux ((e.symm.trans f).trans e) = -(-1 * signAux ((e.symm.trans f).trans e))
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
hefx : ↑e x ≠ ↑e (↑f x)
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
rw [if_neg hfx, ← signAux_eq_signAux2 _ _ e hy, this, signAux_mul, signAux_swap hefx]
no goals
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
hefx : ↑e x ≠ ↑e (↑f x)
⊢ signAux ((e.symm.trans f).trans e) = -(-1 * signAux ((e.symm.trans f).trans e))
simp only [neg_neg, one_mul, neg_mul]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑((e.symm.trans (swap x (↑f x) * f)).trans e) x✝) = ↑(↑(swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e) x✝)
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
⊢ (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
ext
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑((e.symm.trans (f.trans (swap x (↑f x)))).trans e) x✝) =
    ↑(↑(((e.symm.trans f).trans e).trans (swap (↑e x) (↑e (↑f x)))) x✝)
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑((e.symm.trans (swap x (↑f x) * f)).trans e) x✝) = ↑(↑(swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e) x✝)
rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑f (↑e.symm x✝))))
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑((e.symm.trans (f.trans (swap x (↑f x)))).trans e) x✝) =
    ↑(↑(((e.symm.trans f).trans e).trans (swap (↑e x) (↑e (↑f x)))) x✝)
repeat (rw [trans_apply])
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (if ↑f (↑e.symm x✝) = x then ↑f x else if ↑e.symm x✝ = x then x else ↑f (↑e.symm x✝))) =
    ↑(if ↑f (↑e.symm x✝) = x then ↑e (↑f x) else if ↑e.symm x✝ = x then ↑e x else ↑e (↑f (↑e.symm x✝)))
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑f (↑e.symm x✝))))
simp [swap, swapCore]
no goals
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (if ↑f (↑e.symm x✝) = x then ↑f x else if ↑e.symm x✝ = x then x else ↑f (↑e.symm x✝))) =
    ↑(if ↑f (↑e.symm x✝) = x then ↑e (↑f x) else if ↑e.symm x✝ = x then ↑e x else ↑e (↑f (↑e.symm x✝)))
split_ifs <;> rfl
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑f (↑e.symm x✝))))
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑f (↑e.symm x✝))))
(rw [trans_apply])
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑f (↑e.symm x✝))))
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑f (↑e.symm x✝))))
rw [trans_apply]