-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
n m k : ℕ
hn : n = m + k
i : Fin n
⊢ (HMul.hMul (α := (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)[X])
          (Polynomial.map (R := MvPolynomial (Fin m) R)
            (RingHom.comp
              (↑Algebra.TensorProduct.includeLeft :
                MvPolynomial (Fin m) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
              (map (algebraMap R S)))
            (freeMonic R m))
          (Polynomial.map (R := MvPolynomial (Fin k) R)
            (RingHom.comp
              (↑Algebra.TensorProduct.includeRight :
                MvPolynomial (Fin k) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
              (map (algebraMap R S)))
            (freeMonic R k))).coeff
      (↑i : ℕ) =
    (HMul.hMul (α := (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)[X])
          (Polynomial.map
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(Algebra.TensorProduct.lift
                      (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                      (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                        (mapAlgHom (Algebra.ofId R S)))
                      ⋯ :
                    AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                      (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+*
                  MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
              (↑Algebra.TensorProduct.includeLeft :
                MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
            (freeMonic R m))
          (Polynomial.map
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(Algebra.TensorProduct.lift
                      (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
                      (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight)
                        (mapAlgHom (Algebra.ofId R S)))
                      ⋯ :
                    AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                      (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
                MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+*
                  MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
              (↑Algebra.TensorProduct.includeRight :
                MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
            (freeMonic R k))).coeff
      (↑i : ℕ)
have hX : Eq (α := (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)[X])
  (Polynomial.map (R := MvPolynomial (Fin m) R)
    (RingHom.comp
      (↑Algebra.TensorProduct.includeLeft :
        MvPolynomial (Fin m) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
      (map (algebraMap R S)))
    (freeMonic R m))
  (Polynomial.map
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(Algebra.TensorProduct.lift (AlgHom.comp Algebra.TensorProduct.includeLeft (mapAlgHom (Algebra.ofId R S)))
              (AlgHom.comp (AlgHom.restrictScalars R Algebra.TensorProduct.includeRight) (mapAlgHom (Algebra.ofId R S)))
              sorry :
            AlgHom.{u_1, u_1, u_2} R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
              (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)) :
        MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
      (↑Algebra.TensorProduct.includeLeft :
        MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
    (freeMonic R m))
Tactic: congr 2