-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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]) }
⊢ (↑((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])
have 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)
              sorry :
            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)
              sorry :
            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])
Tactic: simp only [universalFactorizationMap, coe_mapEquivMonic_comp, Equiv.apply_symm_apply,
      Polynomial.map_mul]