-- 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 R n
f : 𝓡 →ₐ[R] S
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_2 : 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))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_4 : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
refine_1 :
  Eq (α := MvPolynomial (Fin m) R →ₐ[R] S)
    (AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (AlgHom.restrictScalars R (S := MvPolynomial (Fin n) R)
        (AlgHom.comp (B := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
          (AlgHom.restrictScalars (MvPolynomial (Fin n) R) (S := R)
            ((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))
              ((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]) }))
                f)))
          Algebra.TensorProduct.includeRight))
      Algebra.TensorProduct.includeLeft)
    (AlgHom.comp
      (AlgHom.restrictScalars R
        (AlgHom.comp (AlgHom.restrictScalars (MvPolynomial (Fin n) R) f) Algebra.TensorProduct.includeRight))
      Algebra.TensorProduct.includeLeft)
refine_2 :
  Eq (α := MvPolynomial (Fin k) R →ₐ[R] S)
    (AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      (AlgHom.restrictScalars R
        (AlgHom.restrictScalars R (S := MvPolynomial (Fin n) R)
          (AlgHom.comp (B := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
            (AlgHom.restrictScalars (MvPolynomial (Fin n) R) (S := R)
              ((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))
                ((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]) }))
                  f)))
            Algebra.TensorProduct.includeRight)))
      Algebra.TensorProduct.includeRight)
    (AlgHom.comp
      (AlgHom.restrictScalars R
        (AlgHom.restrictScalars R
          (AlgHom.comp (AlgHom.restrictScalars (MvPolynomial (Fin n) R) f) Algebra.TensorProduct.includeRight)))
      Algebra.TensorProduct.includeRight)
⊢ Eq (α := AlgHom.{u_1, u_1, u_2} (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) S)
    (AlgHom.comp (B := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
      (AlgHom.restrictScalars (MvPolynomial (Fin n) R) (S := R)
        ((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))
          ((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]) }))
            f)))
      Algebra.TensorProduct.includeRight)
    (AlgHom.comp (AlgHom.restrictScalars (MvPolynomial (Fin n) R) f) Algebra.TensorProduct.includeRight)

Tactic:
refine AlgHom.restrictScalars_injective R (Algebra.TensorProduct.ext ?_ ?_)

Premises used: AlgHom.restrictScalars_injective, Algebra.TensorProduct.ext