-- 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 :
  resultant
      (Polynomial.map
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (↑(aeval
                (Algebra.Generators.val
                  (Algebra.Presentation.toGenerators
                    (Algebra.PreSubmersivePresentation.toPresentation
                      (universalFactorizationMapPresentation R n m k hn))))) :
            MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+*
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (↑(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
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (↑(aeval
                (Algebra.Generators.val
                  (Algebra.Presentation.toGenerators
                    (Algebra.PreSubmersivePresentation.toPresentation
                      (universalFactorizationMapPresentation R n m k hn))))) :
            MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+*
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (↑(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 =
    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))
⊢ (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) =
    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))

Tactic:
rw [← (aeval _).coe_toRingHom, ← Polynomial.resultant_map_map,
    Polynomial.map_map, Polynomial.map_map]

Premises used: AlgHom.coe_toRingHom, MvPolynomial.aeval, Polynomial.resultant_map_map, Polynomial.map_map