-- 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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R n m k hn))
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
e_a :
  ∀ (i : Fin m),
    Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (AlgHom.comp
                (AlgHom.comp (B := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
                  (AlgHom.restrictScalars R
                    (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)))
                  (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))))
                (↑(tensorEquivSum R (Fin m) (Fin k) R) :
                  MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R))
              Algebra.TensorProduct.includeLeft :
            (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X i) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((AlgHom.comp (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
              Algebra.TensorProduct.includeLeft :
            (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X i) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
e_a₁ :
  ∀ (i : Fin k),
    Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (AlgHom.restrictScalars R
                (AlgHom.comp
                  (AlgHom.comp (B := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
                    (AlgHom.restrictScalars R
                      (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)))
                    (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))))
                  (↑(tensorEquivSum R (Fin m) (Fin k) R) :
                    MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R)))
              Algebra.TensorProduct.includeRight :
            (a : MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X i) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
      ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)))
              Algebra.TensorProduct.includeRight :
            (a : MvPolynomial (Fin k) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X i) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (AlgHom.comp
      (AlgHom.comp (B := MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
        (AlgHom.restrictScalars R (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)))
        (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))))
      (↑(tensorEquivSum R (Fin m) (Fin k) R) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R))
    (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))

Tactic:
ext