-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hφD :
  Finset.image
      (fun (x : (_ : Fin n) × Fin n) ↦
        Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
          (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
          (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
      D =
    D
x : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : x₂ < x₁
inl :
  ∀ (hlt : LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) x₁ : Fin n) ((σ : (a : Fin n) → Fin n) x₂ : Fin n)),
    f
        ((σ : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
        ((σ : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))) =
      (↑(↑(if
                    LT.lt (α := Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n)
                          (Sigma.snd (α := Fin n) (β := fun (i : Fin n) ↦ Fin n)
                            (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
                                (max
                                  ((σ : (a : Fin n) → Fin n)
                                    (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                  ((σ : (a : Fin n) → Fin n)
                                    (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
                                (min
                                  ((σ : (a : Fin n) → Fin n)
                                    (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                  ((σ : (a : Fin n) → Fin n)
                                    (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))) :
                              (_ : Fin n) × Fin n)) :
                        Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n)
                          (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                            (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
                              (max
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
                              (min
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))))) :
                        Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f
          (Sigma.snd (α := Fin n) (β := fun (i : Fin n) ↦ Fin n)
            (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
                (max
                  ((σ : (a : Fin n) → Fin n)
                    (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                  ((σ : (a : Fin n) → Fin n)
                    (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
                (min
                  ((σ : (a : Fin n) → Fin n)
                    (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                  ((σ : (a : Fin n) → Fin n)
                    (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))) :
              (_ : Fin n) × Fin n))
          (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
            (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
              (max
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
              (min
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))))
inr :
  ∀ (hle : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) x₂ : Fin n) ((σ : (a : Fin n) → Fin n) x₁ : Fin n)),
    f
        ((σ : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
        ((σ : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))) =
      (↑(↑(if
                    LT.lt (α := Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n)
                          (Sigma.snd (α := Fin n) (β := fun (i : Fin n) ↦ Fin n)
                            (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
                                (max
                                  ((σ : (a : Fin n) → Fin n)
                                    (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                  ((σ : (a : Fin n) → Fin n)
                                    (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
                                (min
                                  ((σ : (a : Fin n) → Fin n)
                                    (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                  ((σ : (a : Fin n) → Fin n)
                                    (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))) :
                              (_ : Fin n) × Fin n)) :
                        Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n)
                          (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                            (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
                              (max
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
                              (min
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))))) :
                        Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f
          (Sigma.snd (α := Fin n) (β := fun (i : Fin n) ↦ Fin n)
            (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
                (max
                  ((σ : (a : Fin n) → Fin n)
                    (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                  ((σ : (a : Fin n) → Fin n)
                    (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
                (min
                  ((σ : (a : Fin n) → Fin n)
                    (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                  ((σ : (a : Fin n) → Fin n)
                    (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))) :
              (_ : Fin n) × Fin n))
          (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
            (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
              (max
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
              (min
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))))
⊢ f
      ((σ : (a : Fin n) → Fin n)
        (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
      ((σ : (a : Fin n) → Fin n)
        (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))) =
    (↑(↑(if
                  LT.lt (α := Fin n)
                    ((σ⁻¹ : (a : Fin n) → Fin n)
                        (Sigma.snd (α := Fin n) (β := fun (i : Fin n) ↦ Fin n)
                          (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
                              (max
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
                              (min
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                                ((σ : (a : Fin n) → Fin n)
                                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                    (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))) :
                            (_ : Fin n) × Fin n)) :
                      Fin n)
                    ((σ⁻¹ : (a : Fin n) → Fin n)
                        (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                          (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
                            (max
                              ((σ : (a : Fin n) → Fin n)
                                (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                  (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                              ((σ : (a : Fin n) → Fin n)
                                (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                  (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
                            (min
                              ((σ : (a : Fin n) → Fin n)
                                (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
                                  (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                              ((σ : (a : Fin n) → Fin n)
                                (Sigma.snd (β := fun (i : Fin n) ↦ Fin n)
                                  (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))))) :
                      Fin n) then
                1
              else -1) :
            ℤ) :
        R) *
      f
        (Sigma.snd (α := Fin n) (β := fun (i : Fin n) ↦ Fin n)
          (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
              (max
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
              (min
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
                ((σ : (a : Fin n) → Fin n)
                  (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))) :
            (_ : Fin n) × Fin n))
        (Sigma.fst (β := fun (i : Fin n) ↦ Fin n)
          (Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
            (max
              ((σ : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
              ((σ : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))
            (min
              ((σ : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂)))
              ((σ : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (i : Fin n) ↦ Fin n) (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂))))))

Tactic:
obtain hlt | hle := lt_or_ge (σ x₁) (σ x₂)

Premises used: lt_or_ge, DFunLike.coe