α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 0
_hxy✝ : x ≠ y
⊢ signAux (swap x y) = -1
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 0
⊢ x ≠ y → signAux (swap x y) = -1
intro
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 0
_hxy✝ : x ≠ y
⊢ signAux (swap x y) = -1
exact Fin.elim0 x
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 1
⊢ ¬x = y →
    (∏ x_1 in finPairsLT 1,
        if
            (if x_1.fst = x then y else if x_1.fst = y then x else x_1.fst) ≤
              if x_1.snd = x then y else if x_1.snd = y then x else x_1.snd then
          -1
        else 1) =
      -1
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 1
⊢ x ≠ y → signAux (swap x y) = -1
dsimp [signAux, swap, swapCore]
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 1
⊢ ¬x = y →
    (∏ x_1 in finPairsLT 1,
        if
            (if x_1.fst = x then y else if x_1.fst = y then x else x_1.fst) ≤
              if x_1.snd = x then y else if x_1.snd = y then x else x_1.snd then
          -1
        else 1) =
      -1
simp only [eq_iff_true_of_subsingleton, not_true, ite_true, le_refl, prod_const,
           IsEmpty.forall_iff]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ signAux (swap x y) = -1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ signAux (swap x y) = -1
have h2n : 2 ≤ n + 2 := by exact le_add_self
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (signAux (swap x y))
    (signAux (swap { val := 0, isLt := (_ : 0 < n + 2) } { val := 1, isLt := (_ : 1 < n + 2) }))
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ signAux (swap x y) = -1
rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (signAux (swap x y))
    (signAux (swap { val := 0, isLt := (_ : 0 < n + 2) } { val := 1, isLt := (_ : 1 < n + 2) }))
exact (MonoidHom.mk' signAux signAux_mul).map_isConj
  (isConj_swap hxy (by exact of_decide_eq_true rfl))
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ 2 ≤ n + 2
exact le_add_self
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ { val := 0, isLt := (_ : 0 < n + 2) } ≠ { val := 1, isLt := (_ : 1 < n + 2) }
exact of_decide_eq_true rfl