-- Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Goal:
R : Type u_1
inst : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom
    (↑(universalFactorizationMap R n m k hn) :
      MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x)
H :
  ∀ (i : Fin m ⊕ Fin k),
    Eq (α := MvPolynomial (Fin m ⊕ Fin k) R)
      ((tensorEquivSum R (Fin m) (Fin k) R :
            (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m ⊕ Fin k) R)
          ((f :
              (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) →
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (X i)) :
        MvPolynomial (Fin m ⊕ Fin k) R)
      (X i : MvPolynomial (Fin m ⊕ Fin k) R)
i : Fin n
p : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
a :
  ∀ (i : Fin m),
    Eq (α := 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)
      ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (AlgHom.comp (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x))
                (↑(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)
a₁ :
  ∀ (i : Fin k),
    Eq (α := 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)
      ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (AlgHom.restrictScalars R
                (AlgHom.comp (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x))
                  (↑(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)
⊢ Eq (α := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
    (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
    (AlgHom.comp (aeval (Sum.elim (fun (x : Fin m) ↦ X x ⊗ₜ[R] 1) fun (x : Fin k) ↦ 1 ⊗ₜ[R] X x))
      (↑(tensorEquivSum R (Fin m) (Fin k) R) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] MvPolynomial (Fin m ⊕ Fin k) R))

Tactic:
ext