-- 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
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))
a :
  ∀ (n_1 : ℕ),
    coeff
        (↑(↑(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 : ℕ))
                                            ⋯ :
                                          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
                                      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S),
                                  commutes' := ⋯ :
                                  AlgHom.{u_1, u_1, u_2} (MvPolynomial (Fin n) R)
                                    (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) S }
                                ⋯ :
                              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 : ℕ))
                                            ⋯ :
                                          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
                                      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S),
                                  commutes' := ⋯ :
                                  AlgHom.{u_1, u_1, u_2} (MvPolynomial (Fin n) R)
                                    (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) S }
                                ⋯ :
                              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 S m × MonicDegreeEq S k).1 :
          S[X])
        n_1 =
      (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X]).coeff n_1
a₁ :
  ∀ (n_1 : ℕ),
    coeff
        (↑(↑(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 : ℕ))
                                            ⋯ :
                                          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
                                      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S),
                                  commutes' := ⋯ :
                                  AlgHom.{u_1, u_1, u_2} (MvPolynomial (Fin n) R)
                                    (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) S }
                                ⋯ :
                              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 : ℕ))
                                            ⋯ :
                                          MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
                                      MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S),
                                  commutes' := ⋯ :
                                  AlgHom.{u_1, u_1, u_2} (MvPolynomial (Fin n) R)
                                    (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) S }
                                ⋯ :
                              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 S m × MonicDegreeEq S k).2 :
          S[X])
        n_1 =
      (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).2 : S[X]).coeff n_1
⊢ 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 : ℕ))
                              ⋯ :
                            MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
                        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S),
                    commutes' := ⋯ }
                  ⋯ :
                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 : ℕ))
                              ⋯ :
                            MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) :
                        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* S),
                    commutes' := ⋯ }
                  ⋯ :
                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))
      ⋯ =
    q

Tactic:
ext