-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq S n
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }
simp :
  HMul.hMul (α := S[X])
      (Polynomial.map
        (↑(Algebra.TensorProduct.lift
                ((Equiv.symm (mapEquivMonic R S m) : (a : MonicDegreeEq S m) → MvPolynomial (Fin m) R →ₐ[R] S)
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k).1)
                ((Equiv.symm (mapEquivMonic R S k) : (a : MonicDegreeEq S k) → MvPolynomial (Fin k) R →ₐ[R] S)
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k).2)
                ⋯ :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S)
        (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m :
                (a : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                  MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m)
              Algebra.TensorProduct.includeLeft) :
          (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X]))
      (Polynomial.map
        (↑(Algebra.TensorProduct.lift
                ((Equiv.symm (mapEquivMonic R S m) : (a : MonicDegreeEq S m) → MvPolynomial (Fin m) R →ₐ[R] S)
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k).1)
                ((Equiv.symm (mapEquivMonic R S k) : (a : MonicDegreeEq S k) → MvPolynomial (Fin k) R →ₐ[R] S)
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k).2)
                ⋯ :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S)
        (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k :
                (a : MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →
                  MonicDegreeEq (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
              Algebra.TensorProduct.includeRight) :
          (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])) =
    (↑p : S[X])
⊢ (↑((mapEquivMonic R S n : (a : MvPolynomial (Fin n) R →ₐ[R] S) → MonicDegreeEq S n)
          (AlgHom.comp
            (Algebra.TensorProduct.lift
                ((Equiv.symm (mapEquivMonic R S m) : (a : MonicDegreeEq S m) → MvPolynomial (Fin m) R →ₐ[R] S)
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k).1)
                ((Equiv.symm (mapEquivMonic R S k) : (a : MonicDegreeEq S k) → MvPolynomial (Fin k) R →ₐ[R] S)
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k).2)
                ⋯ :
              MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S)
            (universalFactorizationMap R n m k hn :
              MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))) :
      S[X]) =
    (↑p : S[X])

Tactic:
simp only [universalFactorizationMap, coe_mapEquivMonic_comp, Equiv.apply_symm_apply,
      Polynomial.map_mul]

Premises used: Equiv.apply_symm_apply, Polynomial.map_mul, MvPolynomial.universalFactorizationMap, MvPolynomial.coe_mapEquivMonic_comp