-- 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
⊢ Eq (α := MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
    ((aeval fun (x : Fin n) ↦
            (HMul.hMul (α := (MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)[X])
                  (Polynomial.map
                    (↑Algebra.TensorProduct.includeLeft :
                      MvPolynomial (Fin m) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
                    (freeMonic S m))
                  (Polynomial.map
                    (↑Algebra.TensorProduct.includeRight :
                      MvPolynomial (Fin k) S →+* MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
                    (freeMonic S k))).coeff
              (↑x : ℕ) :
          (a : MvPolynomial (Fin n) S) → MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
        (((map (algebraMap R S) : RingHom.{u_1, u_2} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) S)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) S)
          (X i)) :
      MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
    (((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)) :
          (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
        ((aeval fun (x : Fin n) ↦
              (HMul.hMul (α := (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)[X])
                    (Polynomial.map
                      (↑Algebra.TensorProduct.includeLeft :
                        MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                      (freeMonic R m))
                    (Polynomial.map
                      (↑Algebra.TensorProduct.includeRight :
                        MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
                      (freeMonic R k))).coeff
                (↑x : ℕ) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
          (X i)) :
      MvPolynomial (Fin m) S ⊗[S] MvPolynomial (Fin k) S)
have hX : (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)))
                    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))
        (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.includeRight :
              MvPolynomial (Fin k) R →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
          (freeMonic R k))).coeff
    (↑i : ℕ)
Tactic: simp only [map_X, aeval_X, ← AlgHom.coe_toRingHom, ← Polynomial.coeff_map, Polynomial.map_mul,
      Polynomial.map_map, ← map_map_freeMonic (f := algebraMap R S)]