-- 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 R n
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
⊢ (fun (f : 𝓡 →ₐ[R] S) ↦
        (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
            ((factor₁ m k hn p).map (↑f : 𝓡 →+* S), (factor₂ m k hn p).map (↑f : 𝓡 →+* S)) ⋯ :
          { q : MonicDegreeEq S m × MonicDegreeEq S k //
            (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }))
      ((fun
            (q :
              { q : MonicDegreeEq S m × MonicDegreeEq S k //
                (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) ↦
          (Algebra.TensorProduct.lift (Algebra.ofId R S)
              (let __RingHom : RingHom.{u_1, u_2} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) S :=
                AlgHom.toRingHom (R := R)
                  (↑((Equiv.symm
                            (MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))) :
                          (a :
                              { q : MonicDegreeEq S m × MonicDegreeEq S k //
                                (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑(p.map (algebraMap R S)) : S[X]) }) →
                            { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                              f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
                                ((MvPolynomial.mapEquivMonic R S n).symm :
                                    (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                                  (p.map (algebraMap R S)) })
                        q) :
                    MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S);
              { toRingHom := __RingHom, commutes' := ⋯ })
              ⋯ :
            R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →ₐ[R] S))
        q) =
    q
have simp : Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
    (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
    (MonicDegreeEq.map
        (MonicDegreeEq.map (MonicDegreeEq.freeMonic R m)
          (↑(AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                Algebra.TensorProduct.includeLeft) :
            MvPolynomial (Fin m) R →+*
              R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)))
        (↑(Algebra.TensorProduct.lift (Algebra.ofId R S)
                {
                  toRingHom :=
                    (↑(Algebra.TensorProduct.lift
                            (MvPolynomial.aeval fun (x : Fin m) ↦
                              (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X]).coeff (↑x : ℕ))
                            (MvPolynomial.aeval fun (x : Fin k) ↦
                              (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X]).coeff (↑x : ℕ))
                            sorry :
                          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
                      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S),
                  commutes' := sorry }
                sorry :
              R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →ₐ[R] S) :
          R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →+* S),
      MonicDegreeEq.map
        (MonicDegreeEq.map (MonicDegreeEq.freeMonic R k)
          (↑(AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                Algebra.TensorProduct.includeRight) :
            MvPolynomial (Fin k) R →+*
              R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)))
        (↑(Algebra.TensorProduct.lift (Algebra.ofId R S)
                {
                  toRingHom :=
                    (↑(Algebra.TensorProduct.lift
                            (MvPolynomial.aeval fun (x : Fin m) ↦
                              (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X]).coeff (↑x : ℕ))
                            (MvPolynomial.aeval fun (x : Fin k) ↦
                              (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X]).coeff (↑x : ℕ))
                            sorry :
                          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
                      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S),
                  commutes' := sorry }
                sorry :
              R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →ₐ[R] S) :
          R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →+* S))
    sorry =
  q
Tactic: simp only [UniversalFactorizationRing, MvPolynomial.mapEquivMonic, AlgHom.toRingHom_eq_coe,
      Equiv.coe_fn_symm_mk, MvPolynomial.coe_aeval_eq_eval, factor₁, monicDegreeEq_coe,
      MvPolynomial.universalFactorizationMapLiftEquiv, Equiv.coe_fn_mk, fromTensor,
      MonicDegreeEq.map_coe, factor₂]