-- 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)
neg :
  ∀
    (hf :
      LT.lt (α := Fin n)
        ((f : (a : Fin n) → Fin n)
            ((g : (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)
        ((f : (a : Fin n) → Fin n)
            ((g : (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)),
    (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)
neg₁ :
  ∀
    (hf :
      LT.lt (α := Fin n)
        ((f : (a : Fin n) → Fin n)
            ((g : (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)
            ((g : (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)),
    (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)
⊢ (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:
obtain hf | hf := (f.injective.ne <| g.injective.ne hab.ne).lt_or_gt

Premises used: Function.Injective.ne, Equiv.injective, Ne.lt_or_gt, LT.lt.ne