-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
this : ¬b₁ < b₂
pos :
  LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) →
    LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
      ∀
        (h :
          Eq (α := (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂) :
              (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂) :
              (_ : Fin n) × Fin n)),
        Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
neg :
  LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) →
    ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
      ∀
        (h :
          Eq (α := (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂) :
              (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
              (_ : Fin n) × Fin n)),
        Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
pos₁ :
  ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) →
    LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
      ∀
        (h :
          Eq (α := (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
              (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂) :
              (_ : Fin n) × Fin n)),
        Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
neg₁ :
  ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) →
    ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
      ∀
        (h :
          Eq (α := (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
              (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
              (_ : Fin n) × Fin n)),
        Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)

Tactic:
split_ifs at h