awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
h :
  LT.lt (α := Fin n)
    ((f : (a : Fin n) → Fin n)
        (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
      Fin n)
    ((f : (a : Fin n) → Fin n)
        (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
      Fin n)
⊢ Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
      ((f : (a : Fin n) → Fin n)
        (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
      ((f : (a : Fin n) → Fin n)
        (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) ∈
    finPairsLT n

Tactic:
mem_finPairsLT.2 h

Premises used: Iff.mpr, Equiv.Perm.mem_finPairsLT
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
h :
  LT.lt (α := Fin n)
    ((f : (a : Fin n) → Fin n)
        (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
      Fin n)
    ((f : (a : Fin n) → Fin n)
        (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
      Fin n)
⊢ Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
      ((f : (a : Fin n) → Fin n)
        (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
      ((f : (a : Fin n) → Fin n)
        (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) ∈
    finPairsLT n

Tactic:
exact mem_finPairsLT.2 h

Premises used: Iff.mpr, Equiv.Perm.mem_finPairsLT
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
h :
  ¬LT.lt (α := Fin n)
      ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
        Fin n)
      ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
        Fin n)
⊢ Membership.mem (α := (_ : Fin n) × Fin n) (finPairsLT n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) :
      (_ : Fin n) × Fin n)

Tactic:
mem_finPairsLT.2
        ((le_of_not_gt h).lt_of_ne fun h => (mem_finPairsLT.1 ha).ne (f.injective h.symm))

Premises used: Iff.mpr, le_of_not_gt, LE.le.lt_of_ne, Iff.mp, Equiv.Perm.mem_finPairsLT, Equiv.injective, Eq.symm, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
h :
  ¬LT.lt (α := Fin n)
      ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
        Fin n)
      ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
        Fin n)
⊢ Membership.mem (α := (_ : Fin n) × Fin n) (finPairsLT n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) :
      (_ : Fin n) × Fin n)

Tactic:
exact mem_finPairsLT.2
        ((le_of_not_gt h).lt_of_ne fun h => (mem_finPairsLT.1 ha).ne (f.injective h.symm))

Premises used: Iff.mpr, Equiv.Perm.mem_finPairsLT
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a b : Fin n
hab : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b ∈ finPairsLT n
pos :
  ∀
    (h :
      LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) b : Fin n)
        ((Equiv.symm f : (a : Fin n) → Fin n) a : Fin n)),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin n)
            ((f⁻¹ : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
              Fin n)
            ((f⁻¹ : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
              Fin n) then
        -1
      else 1)
      (if
          LE.le (α := Fin n)
            ((f : (a : Fin n) → Fin n)
                ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
              Fin n)
            ((f : (a : Fin n) → Fin n)
                ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
              Fin n) then
        -1
      else 1)
neg :
  ∀
    (h :
      ¬LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) b : Fin n)
          ((Equiv.symm f : (a : Fin n) → Fin n) a : Fin n)),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin n)
            ((f⁻¹ : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
              Fin n)
            ((f⁻¹ : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
              Fin n) then
        -1
      else 1)
      (if
          LE.le (α := Fin n)
            ((f : (a : Fin n) → Fin n)
                ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
              Fin n)
            ((f : (a : Fin n) → Fin n)
                ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
              Fin n) then
        -1
      else 1)
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n) then
      -1
    else 1)
    (if
        LE.le (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n) then
      -1
    else 1)

Tactic:
by_cases h : f.symm b < f.symm a

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a b : Fin n
hab : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b ∈ finPairsLT n
h : LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) b : Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a : Fin n)
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n) then
      -1
    else 1)
    (if
        LE.le (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n) then
      -1
    else 1)

Tactic:
simp_all [signBijAux, (mem_finPairsLT.1 hab).not_ge]

Premises used: Iff.mp, Equiv.Perm.mem_finPairsLT, Equiv.Perm.signBijAux, LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a b : Fin n
hab : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b ∈ finPairsLT n
h :
  ¬LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) b : Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a : Fin n)
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n) then
      -1
    else 1)
    (if
        LE.le (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n) then
      -1
    else 1)

Tactic:
simp_all [signBijAux, dif_neg h, (mem_finPairsLT.1 hab).le]

Premises used: LT.lt.le, dif_neg, Iff.mp, Equiv.Perm.mem_finPairsLT, Equiv.Perm.signBijAux
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f g : Perm (Fin n)
rw : (f * g).signAux = f.signAux * g⁻¹.signAux
⊢ (f * g).signAux = f.signAux * g.signAux

Tactic:
rw [← signAux_inv g]

Premises used: Equiv.Perm.signAux_inv
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f g : Perm (Fin n)
rw :
  Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f * g : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ x ∈ finPairsLT n,
      HMul.hMul (α := ℤˣ)
        (if
            LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((f : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
        (if
            LE.le (α := Fin n) ((g⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((g⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1))
⊢ (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f * g : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1) =
    HMul.hMul (α := ℤˣ)
      (∏ x ∈ finPairsLT n,
        if
            LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((f : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
      (∏ x ∈ finPairsLT n,
        if
            LE.le (α := Fin n) ((g⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((g⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)

Tactic:
rw [← prod_mul_distrib]

Premises used: Finset.prod_mul_distrib
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f g : Perm (Fin n)
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f * g : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ x ∈ finPairsLT n,
      HMul.hMul (α := ℤˣ)
        (if
            LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((f : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
        (if
            LE.le (α := Fin n) ((g⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((g⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1))

Tactic:
prod_nbij (signBijAux g) signBijAux_mem signBijAux_injOn signBijAux_surj ?_

Premises used: Equiv.Perm.signBijAux_surj, Equiv.Perm.signBijAux, Equiv.Perm.signBijAux_mem, Finset.prod_nbij, Equiv.Perm.signBijAux_injOn
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f g : Perm (Fin n)
refine :
  ∀ a ∈ finPairsLT n,
    (if
          LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (a.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f * g : (a : Fin n) → Fin n) (a.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1) =
      HMul.hMul (α := ℤˣ)
        (if
            LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) ((g.signBijAux a).fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((f : (a : Fin n) → Fin n) ((g.signBijAux a).snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
        (if
            LE.le (α := Fin n)
              ((g⁻¹ : (a : Fin n) → Fin n) ((g.signBijAux a).fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((g⁻¹ : (a : Fin n) → Fin n) ((g.signBijAux a).snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f * g : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ x ∈ finPairsLT n,
      HMul.hMul (α := ℤˣ)
        (if
            LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((f : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
        (if
            LE.le (α := Fin n) ((g⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((g⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1))

Tactic:
refine prod_nbij (signBijAux g) signBijAux_mem signBijAux_injOn signBijAux_surj ?_

Premises used: Equiv.Perm.signBijAux_surj, Equiv.Perm.signBijAux, Equiv.Perm.signBijAux_mem, Finset.prod_nbij, Equiv.Perm.signBijAux_injOn
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b ∈ finPairsLT n
⊢ Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)

Tactic:
rw [mem_finPairsLT] at hab

Premises used: Equiv.Perm.mem_finPairsLT
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)
hg : LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n) ((g : (a : Fin n) → Fin n) a : Fin n)
⊢ (if
        LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) ((g : (a : Fin n) → Fin n) a) : Fin n)
          ((f : (a : Fin n) → Fin n) ((g : (a : Fin n) → Fin n) b) : Fin n) then
      -1
    else 1) =
    HMul.hMul (α := ℤˣ)
      (if
          LE.le (α := Fin n)
            ((f : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (x : Fin n) ↦ Fin n)
                  (if x :
                      LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n)
                        ((g : (a : Fin n) → Fin n) a : Fin n) then
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) a) ((g : (a : Fin n) → Fin n) b)
                  else
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) b)
                      ((g : (a : Fin n) → Fin n) a))) :
              Fin n)
            ((f : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (x : Fin n) ↦ Fin n)
                  (if x :
                      LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n)
                        ((g : (a : Fin n) → Fin n) a : Fin n) then
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) a) ((g : (a : Fin n) → Fin n) b)
                  else
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) b)
                      ((g : (a : Fin n) → Fin n) a))) :
              Fin n) then
        -1
      else 1)
      (if
          LE.le (α := Fin n)
            ((g⁻¹ : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (x : Fin n) ↦ Fin n)
                  (if x :
                      LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n)
                        ((g : (a : Fin n) → Fin n) a : Fin n) then
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) a) ((g : (a : Fin n) → Fin n) b)
                  else
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) b)
                      ((g : (a : Fin n) → Fin n) a))) :
              Fin n)
            ((g⁻¹ : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (x : Fin n) ↦ Fin n)
                  (if x :
                      LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n)
                        ((g : (a : Fin n) → Fin n) a : Fin n) then
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) a) ((g : (a : Fin n) → Fin n) b)
                  else
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) b)
                      ((g : (a : Fin n) → Fin n) a))) :
              Fin n) then
        -1
      else 1)

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
x : (_ : Fin (n + 2)) × Fin (n + 2)
x₁ x₂ : Fin (n + 2)
⊢ Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2)))
      {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
      (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) x₁ x₂) →
    Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2))
      (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) x₁ x₂)

Tactic:
simp +contextual [mem_finPairsLT]

Premises used: Equiv.Perm.mem_finPairsLT
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
refine :
  ∀ (a : (_ : Fin (n + 2)) × Fin (n + 2))
    (ha₁ : Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2)) a)
    (ha₂ : a ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (a.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
              Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (a.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
              Fin (n + 2)) then
        -1
      else 1)
      1
⊢ signAux (n := n + 2) (swap 0 1) =
    ∏ x ∈ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0},
      if
          LE.le (α := Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (x.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
              Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (x.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
              Fin (n + 2)) then
        -1
      else 1

Tactic:
refine Eq.symm (prod_subset (fun ⟨x₁, x₂⟩ => by
      simp +contextual [mem_finPairsLT]) fun a ha₁ ha₂ => ?_)

Premises used: Finset.prod_subset, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a : (_ : Fin (n + 2)) × Fin (n + 2)
ha₁ : Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2)) a
ha₂ : a ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
rcases :
  ∀ (a₁ a₂ : Fin (n + 2))
    (ha₁ :
      Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2))
        (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂))
    (ha₂ :
      Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉
        {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
                (Sigma.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                  (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
              Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
                (Sigma.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                  (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
              Fin (n + 2)) then
        -1
      else 1)
      1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (a.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
            Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (a.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
            Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
rcases a with ⟨a₁, a₂⟩
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₁ :
  Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2))
    (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
⊢ a₂ < a₁

Tactic:
replace ha₁ : a₂ < a₁ := mem_finPairsLT.1 ha₁
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
dsimp :
  Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
              (Sigma.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
            Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
              (Sigma.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
            Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
inl :
  ∀
    (ha₂ :
      Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 0 a₂ ∉
        {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0})
    (ha₁ : a₂ < 0),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 : Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
        -1
      else 1)
      1
inr :
  ∀ (H : 0 < a₁),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
        -1
      else 1)
      1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
rcases a₁.zero_le.eq_or_lt with (rfl | H)

Premises used: LE.le.eq_or_lt, Fin.zero_le, rfl