-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
f : 𝓡 →ₐ[R] S
this_1 : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  RingHom.toAlgebra (AlgHom.toRingHom (MvPolynomial.universalFactorizationMap R n m k hn))
this_2 : Algebra (MvPolynomial (Fin n) R) R :=
  RingHom.toAlgebra
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_3 : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) S :=
  Algebra.compHom (R := R) S
    (AlgHom.toRingHom (R := R)
      ((Equiv.symm (MvPolynomial.mapEquivMonic R R n) : (a : MonicDegreeEq R n) → MvPolynomial (Fin n) R →ₐ[R] R) p))
this_4 : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i : Fin k
⊢ Eq.{u_2 + 1} (α := S)
    ((AlgHom.comp (B := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
            (AlgHom.restrictScalars R
              (AlgHom.restrictScalars R (S := MvPolynomial (Fin n) R)
                (AlgHom.comp (B := R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
                  (AlgHom.restrictScalars (MvPolynomial (Fin n) R) (S := R)
                    ((fun
                          (q :
                            { q : MonicDegreeEq S m × MonicDegreeEq S k //
                              (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }) ↦
                        (Algebra.TensorProduct.lift (Algebra.ofId R S)
                            (let __RingHom :
                              RingHom.{u_1, u_2} (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) S :=
                              AlgHom.toRingHom (R := R)
                                (↑((Equiv.symm
                                          (MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn
                                            (p.map (algebraMap R S))) :
                                        (a :
                                            { q : MonicDegreeEq S m × MonicDegreeEq S k //
                                              (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑(p.map (algebraMap R S)) : S[X]) }) →
                                          { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                                            f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
                                              ((MvPolynomial.mapEquivMonic R S n).symm :
                                                  (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                                                (p.map (algebraMap R S)) })
                                      q) :
                                  MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S);
                            { toRingHom := __RingHom, commutes' := ⋯ })
                            ⋯ :
                          R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →ₐ[R] S))
                      ((fun (f : 𝓡 →ₐ[R] S) ↦
                          (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                              (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]))
                              ((factor₁ m k hn p).map (↑f : 𝓡 →+* S), (factor₂ m k hn p).map (↑f : 𝓡 →+* S)) ⋯ :
                            { q : MonicDegreeEq S m × MonicDegreeEq S k //
                              (↑q.1 : S[X]) * (↑q.2 : S[X]) = map (algebraMap R S) (↑p : R[X]) }))
                        f)))
                  Algebra.TensorProduct.includeRight)))
            Algebra.TensorProduct.includeRight :
          (a : MvPolynomial (Fin k) R) → S)
        (MvPolynomial.X i) :
      S)
    ((AlgHom.comp
            (AlgHom.restrictScalars R
              (AlgHom.restrictScalars R
                (AlgHom.comp (AlgHom.restrictScalars (MvPolynomial (Fin n) R) f) Algebra.TensorProduct.includeRight)))
            Algebra.TensorProduct.includeRight :
          (a : MvPolynomial (Fin k) R) → S)
        (MvPolynomial.X i) :
      S)
have refine_2 : Eq.{u_2 + 1} (α := S)
  ((f : (a : 𝓡) → S)
      ((fromTensor m k hn p : (a : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) → 𝓡) (1 ⊗ₜ[R] MvPolynomial.X i) :
        𝓡) :
    S)
  ((f : (a : R ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) → S)
      (1 ⊗ₜ[MvPolynomial (Fin n) R] (1 ⊗ₜ[R] MvPolynomial.X i)) :
    S)
Tactic: simp [MvPolynomial.universalFactorizationMapLiftEquiv, MvPolynomial.mapEquivMonic,
        UniversalFactorizationRing.factor₂, coeff_freeMonic]