-- 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
f :
  { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
    f.comp (universalFactorizationMap R n m k hn) =
      (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p }
a :
  ∀ (i : Fin m),
    Eq.{u_2 + 1} (α := S)
      ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (↑((fun
                        (q :
                          { q : MonicDegreeEq S m × MonicDegreeEq S k //
                            (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }) ↦
                      (Subtype.mk (p := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) ↦
                          f.comp (universalFactorizationMap R n m k hn) =
                            (Equiv.symm (mapEquivMonic R S n) :
                                (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                              p)
                          (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)
                            ⋯)
                          ⋯ :
                        { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                          f.comp (universalFactorizationMap R n m k hn) =
                            (Equiv.symm (mapEquivMonic R S n) :
                                (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                              p }))
                    ((fun
                          (f :
                            { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                              f.comp (universalFactorizationMap R n m k hn) =
                                (Equiv.symm (mapEquivMonic R S n) :
                                    (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                                  p }) ↦
                        (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                            (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]))
                            ((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
                                ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                                  Algebra.TensorProduct.includeLeft),
                              (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
                                ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                                  Algebra.TensorProduct.includeRight))
                            ⋯ :
                          { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }))
                      f)) :
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S)
              Algebra.TensorProduct.includeLeft :
            (a : MvPolynomial (Fin m) R) → S)
          (X i) :
        S)
      (((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp Algebra.TensorProduct.includeLeft :
            (a : MvPolynomial (Fin m) R) → S)
          (X i) :
        S)
a₁ :
  ∀ (i : Fin k),
    Eq.{u_2 + 1} (α := S)
      ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (AlgHom.restrictScalars R (S := R)
                (↑((fun
                          (q :
                            { q : MonicDegreeEq S m × MonicDegreeEq S k //
                              (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }) ↦
                        (Subtype.mk (p := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) ↦
                            f.comp (universalFactorizationMap R n m k hn) =
                              (Equiv.symm (mapEquivMonic R S n) :
                                  (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                                p)
                            (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)
                              ⋯)
                            ⋯ :
                          { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                            f.comp (universalFactorizationMap R n m k hn) =
                              (Equiv.symm (mapEquivMonic R S n) :
                                  (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                                p }))
                      ((fun
                            (f :
                              { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                                f.comp (universalFactorizationMap R n m k hn) =
                                  (Equiv.symm (mapEquivMonic R S n) :
                                      (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                                    p }) ↦
                          (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                              (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]))
                              ((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
                                  ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                                    Algebra.TensorProduct.includeLeft),
                                (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
                                  ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                                    Algebra.TensorProduct.includeRight))
                              ⋯ :
                            { q : MonicDegreeEq S m × MonicDegreeEq S k //
                              (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }))
                        f)) :
                  MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S))
              Algebra.TensorProduct.includeRight :
            (a : MvPolynomial (Fin k) R) → S)
          (X i) :
        S)
      ((AlgHom.comp (AlgHom.restrictScalars R (↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S))
              Algebra.TensorProduct.includeRight :
            (a : MvPolynomial (Fin k) R) → S)
          (X i) :
        S)
⊢ (fun (q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }) ↦
        (Subtype.mk (p := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) ↦
            f.comp (universalFactorizationMap R n m k hn) =
              (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p)
            (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)
              ⋯)
            ⋯ :
          { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
            f.comp (universalFactorizationMap R n m k hn) =
              (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p }))
      ((fun
            (f :
              { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                f.comp (universalFactorizationMap R n m k hn) =
                  (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p }) ↦
          (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
              (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]))
              ((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
                  ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                    Algebra.TensorProduct.includeLeft),
                (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
                  ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                    Algebra.TensorProduct.includeRight))
              ⋯ :
            { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }))
        f) =
    f

Tactic:
ext