-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
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)
⊢ 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))
have 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)
Tactic: ext