-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
rw : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
rw₁ : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
rw₂ :
  Matrix.det (n := Fin (m + n))
      ((Matrix.reindex (finCongr ⋯)
            (Equiv.trans (Equiv.symm finSumFinEquiv) (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv)) :
          (a : Matrix (Fin (n + m)) (Fin (n + m)) R) → Matrix (Fin (m + n)) (Fin (m + n)) R)
        (g.sylvester f n m)) =
    HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
rw₃ :
  (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin (n + m))) → ℤˣ)
                (Equiv.trans
                  (Equiv.trans (Equiv.symm finSumFinEquiv) (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                  (Equiv.symm (finCongr ⋯)))) :
            ℤ) :
        R) *
      (g.sylvester f n m).det =
    HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
rw₄ rw₅ rw₆ :
  (↑(↑(∏ i : Fin (n + m),
                ∏ j ∈ Finset.Ioi i,
                  if
                      LT.lt (α := Fin (n + m))
                        ((Equiv.trans
                                (Equiv.trans (Equiv.symm finSumFinEquiv)
                                  (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                                (Equiv.symm (finCongr ⋯)) :
                              (a : Fin (n + m)) → Fin (n + m))
                            i :
                          Fin (n + m))
                        ((Equiv.trans
                                (Equiv.trans (Equiv.symm finSumFinEquiv)
                                  (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                                (Equiv.symm (finCongr ⋯)) :
                              (a : Fin (n + m)) → Fin (n + m))
                            j :
                          Fin (n + m)) then
                    1
                  else -1) :
            ℤ) :
        R) *
      (g.sylvester f n m).det =
    HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
e_a :
  (↑(↑(∏ i : Fin (n + m),
              ∏ j ∈ Finset.Ioi i,
                if
                    LT.lt (α := Fin (n + m))
                      ((Equiv.trans
                              (Equiv.trans (Equiv.symm finSumFinEquiv)
                                (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                              (Equiv.symm (finCongr ⋯)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          i :
                        Fin (n + m))
                      ((Equiv.trans
                              (Equiv.trans (Equiv.symm finSumFinEquiv)
                                (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                              (Equiv.symm (finCongr ⋯)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          j :
                        Fin (n + m)) then
                  1
                else -1) :
          ℤ) :
      R) =
    HPow.hPow (α := R) (-1) (m * n)
e_a₁ :
  (↑(↑(∏ i : Fin (n + m),
              ∏ j ∈ Finset.Ioi i,
                if
                    Fin.cast ⋯
                        ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                          (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) i))) <
                      Fin.cast ⋯
                        ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                          (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) j))) then
                  1
                else -1) :
          ℤ) :
      R) =
    HPow.hPow (α := R) (-1) (m * n)
e_a₂ :
  (∏ x : Fin (n + m),
      ∏ x_1 ∈ Finset.Ioi x,
        if
            LT.lt (α := Fin (m + n))
              ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                  (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x)) :
                Fin (m + n))
              ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                  (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x_1)) :
                Fin (m + n)) then
          1
        else -1) =
    HPow.hPow (α := R) (-1) (m * n)
e_a₃ :
  ∏ x : Fin n ⊕ Fin m,
      Finset.prod (ι := Fin n ⊕ Fin m)
        (Finset.map (Equiv.toEmbedding (Equiv.symm finSumFinEquiv))
          (Finset.Ioi ((finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m)) x)))
        ((fun (x_1 : Fin (n + m)) ↦
            if
                LT.lt (α := Fin (m + n))
                  ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                      (Sum.swap
                        ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m)
                          ((finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m)) x : Fin (n + m)))) :
                    Fin (m + n))
                  ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                      (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x_1)) :
                    Fin (m + n)) then
              1
            else -1) ∘
          (⇑(Equiv.symm (Equiv.symm finSumFinEquiv)) : (a : Fin n ⊕ Fin m) → Fin (n + m))) =
    HPow.hPow (α := R) (-1) (m * n)
e_a₄ :
  HMul.hMul (α := R)
      (∏ x : Fin n,
        HMul.hMul (α := R) (∏ x : Fin n, if False then -1 else 1)
          (∏ x_1 : Fin m, if (↑x : ℕ) < n + (↑x_1 : ℕ) ∧ ¬m + (↑x : ℕ) < (↑x_1 : ℕ) then -1 else 1))
      (∏ x : Fin m,
        HMul.hMul (α := R) (∏ x_1 : Fin n, if n + (↑x : ℕ) < (↑x_1 : ℕ) ∧ ¬(↑x : ℕ) < m + (↑x_1 : ℕ) then -1 else 1)
          (∏ x : Fin m, if False then -1 else 1)) =
    HPow.hPow (α := R) (-1) (m * n)
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m

Tactic:
classical
  rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]
  congr 1
  dsimp
  simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]
  simp_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]
  simp only [Equiv.symm_apply_apply, ← Fin.val_fin_lt, Equiv.symm_symm, Function.comp_apply,
    ← Finset.prod_ite_mem_eq (Finset.map _ _), Finset.mem_map_equiv, Finset.mem_Ioi,
    Fintype.prod_sum_type, finSumFinEquiv_apply_left, Fin.val_castAdd, Sum.swap_inl,
    finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.swap_inr, add_lt_add_iff_left,
    ← ite_not (α := R) (p := _ < _) (y := 1), ← ite_and, and_not_self]
  simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, pow_mul]

Premises used: Int.cast_neg, Fin.val_fin_lt, finSumFinEquiv_apply_left, Polynomial.sylvester_comm, Polynomial.resultant, Sum.swap_inr, Equiv.symm_apply_apply, Equiv.Perm.sign_eq_prod_prod_Ioi, Int.reduceNeg, Units.coe_prod, Finset.map, Fin.isLt, finSumFinEquiv_apply_right, apply_ite, Equiv.symm_symm, LT.lt.le, Matrix.det_reindex, pow_mul, Finset.mem_Ioi, Finset.mem_map_equiv, Units.val_neg, Fin.val_castAdd, Equiv.prod_comp, and_not_self, LT.lt.trans_le, LT.lt, finSumFinEquiv, Units.val_one, ite_not, Finset.prod_ite_mem_eq, Function.comp_apply, LE.le.trans, Equiv.symm, Fin.cast_lt_cast, ite_and, Polynomial.natDegree, OfNat.ofNat, Fintype.prod_sum_type, Fin.val_natAdd, Finset.prod_map_equiv, Int.cast_prod, Int.cast_one, add_lt_add_iff_left, Sum.swap_inl