-- 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) 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)
have 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)
Tactic: rw [mul_apply, mul_apply]