-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (universalFactorizationMap R (m + k) m k ⋯))
i j : Fin (m + k)
⊢ Eq (α :=
    Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
      (Algebra.Presentation.toGenerators
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k ⋯))))
    (Algebra.PreSubmersivePresentation.jacobiMatrix (universalFactorizationMapPresentation R (m + k) m k ⋯) i j)
    (-Fin.addCases (motive := fun (x : Fin (m + k)) ↦ MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
        (fun (j₁ : Fin m) ↦
          if (↑j : ℕ) ∈ Set.Icc (↑j₁ : ℕ) ((↑j₁ : ℕ) + k) then
            Polynomial.coeff
              (Polynomial.map
                (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inr)) :
                  MvPolynomial (Fin k) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
                (freeMonic R k))
              ((↑j : ℕ) - (↑j₁ : ℕ))
          else 0)
        (fun (j₁ : Fin k) ↦
          if (↑j : ℕ) ∈ Set.Icc (↑j₁ : ℕ) ((↑j₁ : ℕ) + m) then
            Polynomial.coeff
              (Polynomial.map
                (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inl)) :
                  MvPolynomial (Fin m) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
                (freeMonic R m))
              ((↑j : ℕ) - (↑j₁ : ℕ))
          else 0)
        i)
have a : Eq (α :=
  Algebra.Generators.Ring (R := MvPolynomial (Fin (m + k)) R)
    (Algebra.Presentation.toGenerators
      (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k sorry))))
  ((pderiv
          (Algebra.PreSubmersivePresentation.map (R := MvPolynomial (Fin (m + k)) R)
            (universalFactorizationMapPresentation R (m + k) m k sorry) i) :
        (a : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R)) →
          MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
      (Algebra.Presentation.relation
        (Algebra.PreSubmersivePresentation.toPresentation (universalFactorizationMapPresentation R (m + k) m k sorry)) j) :
    MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
  (-Fin.addCases (motive := fun (x : Fin (m + k)) ↦ MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
        (fun (j₁ : Fin m) ↦
          if (↑j : ℕ) ∈ Set.Icc (↑j₁ : ℕ) ((↑j₁ : ℕ) + k) then
            Polynomial.coeff
              (Polynomial.map
                (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inr)) :
                  MvPolynomial (Fin k) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
                (freeMonic R k))
              ((↑j : ℕ) - (↑j₁ : ℕ))
          else 0)
        (fun (j₁ : Fin k) ↦
          if (↑j : ℕ) ∈ Set.Icc (↑j₁ : ℕ) ((↑j₁ : ℕ) + m) then
            Polynomial.coeff
              (Polynomial.map
                (↑(AlgHom.comp (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin (m + k)) R))) (rename Sum.inl)) :
                  MvPolynomial (Fin m) R →+* MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
                (freeMonic R m))
              ((↑j : ℕ) - (↑j₁ : ℕ))
          else 0)
        i :
    MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin (m + k)) R))
Tactic: rw [Algebra.PreSubmersivePresentation.jacobiMatrix_apply]