-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
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)
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
have 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)
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]