-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b ∈ finPairsLT n
⊢ (if
        LE.le (α := Fin n)
          ((f * 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 * 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) then
      -1
    else 1) =
    HMul.hMul (α := ℤˣ)
      (if
          LE.le (α := Fin n)
            ((f : (a : Fin n) → Fin n)
                ((g.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)
                ((g.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).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 (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
              Fin n)
            ((g⁻¹ : (a : Fin n) → Fin n)
                ((g.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
              Fin n) then
        -1
      else 1)
have dsimp : (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: dsimp only [signBijAux]