-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
h : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
inr :
  HMul.hMul (β := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n)
      ((aeval
              (Algebra.Generators.val
                (Algebra.Presentation.toGenerators
                  (Algebra.PreSubmersivePresentation.toPresentation
                    (universalFactorizationMapPresentation R n m k hn)))) :
            (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (resultant
            (Polynomial.map
              (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inl)) :
                MvPolynomial (Fin m) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
              (freeMonic R m))
            (Polynomial.map
              (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inr)) :
                MvPolynomial (Fin k) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
              (freeMonic R k))
            m k) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) =
    HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
      resultant (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
        (Polynomial.map
          (↑Algebra.TensorProduct.includeRight :
            MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (freeMonic R k))
⊢ (algebraMap
          (Algebra.Generators.Ring (R := MvPolynomial (Fin n) R)
            (Algebra.Presentation.toGenerators
              (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R n m k hn))))
          (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :
        (a : (universalFactorizationMapPresentation R n m k hn).Ring) →
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (Matrix.det (n := Fin n)
        (-Matrix.transpose
            ((Matrix.reindex (finCongr ⋯) (finCongr ⋯) :
                (a : Matrix (Fin (m + k)) (Fin (m + k)) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))) →
                  Matrix (Fin n) (Fin n) (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)))
              (sylvester
                (Polynomial.map (R := MvPolynomial (Fin m) R)
                  (AlgHom.toRingHom
                    (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inl)))
                  (freeMonic R m))
                (Polynomial.map (R := MvPolynomial (Fin k) R)
                  (AlgHom.toRingHom
                    (AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))) (rename Sum.inr)))
                  (freeMonic R k))
                m k)))) =
    HPow.hPow (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (-1) n *
      resultant (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m))
        (Polynomial.map (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (freeMonic R k))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, Matrix.det_neg, Matrix.det_transpose, Matrix.det_reindex_self,
    Algebra.Generators.algebraMap_apply, ← Polynomial.resultant.eq_def,
    Fintype.card_fin, map_mul, map_pow, map_neg, map_one]

Premises used: Fintype.card_fin, Matrix.det_transpose, Polynomial.resultant.eq_def, Algebra.Generators.algebraMap_apply, map_neg, map_pow, map_mul, Matrix.det_neg, map_one, Matrix.det_reindex_self, AlgHom.toRingHom_eq_coe