-- 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
rw :
  Eq.{u_1 + 1} (α := R)
    (∏ x ∈ D,
      f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
        ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
    (∏ x ∈ D,
      (↑(↑(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) (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)))) :
                              (_ : 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) (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)))))) :
                        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) (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)))) :
              (_ : 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) (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)))))))
⊢ Eq.{u_1 + 1} (α := R)
    (∏ x ∈ D,
      f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
        ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
    (∏
      x ∈
        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,
      (↑(↑(if
                    LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))

Tactic:
rw [Finset.prod_image fun x hx y hy ↦ Finset.injOn_of_card_image_eq (by rw [hφD]) hx hy]

Premises used: Finset.injOn_of_card_image_eq, Finset.prod_image