-- 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
rw :
  (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 * g : (a : Fin n) → Fin n) a : Fin n) ((f * 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:
rw [mul_apply, mul_apply]

Premises used: Equiv.Perm.mul_apply