-- 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 S n
q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }
⊢ (fun
          (f :
            { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
              f.comp (universalFactorizationMap R n m k hn) =
                (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p }) ↦
        (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦ (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]))
            ((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
                ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                  Algebra.TensorProduct.includeLeft),
              (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
                ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                  Algebra.TensorProduct.includeRight))
            ⋯ :
          { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }))
      ((fun (q : { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }) ↦
          (Subtype.mk (p := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) ↦
              f.comp (universalFactorizationMap R n m k hn) =
                (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p)
              (Algebra.TensorProduct.lift
                ((Equiv.symm (mapEquivMonic R S m) : (a : MonicDegreeEq S m) → MvPolynomial (Fin m) R →ₐ[R] S)
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k).1)
                ((Equiv.symm (mapEquivMonic R S k) : (a : MonicDegreeEq S k) → MvPolynomial (Fin k) R →ₐ[R] S)
                  (↑q : MonicDegreeEq S m × MonicDegreeEq S k).2)
                ⋯)
              ⋯ :
            { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
              f.comp (universalFactorizationMap R n m k hn) =
                (Equiv.symm (mapEquivMonic R S n) : (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S) p }))
        q) =
    q
have a : ∀ (n_1 : ℕ),
  Polynomial.coeff
      (↑(↑((fun
                      (f :
                        { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                          f.comp (universalFactorizationMap R n m k hn) =
                            (Equiv.symm (mapEquivMonic R S n) :
                                (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                              p }) ↦
                    (Subtype.mk (p := fun (q : MonicDegreeEq S m × MonicDegreeEq S k) ↦
                        (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]))
                        ((mapEquivMonic R S m : (a : MvPolynomial (Fin m) R →ₐ[R] S) → MonicDegreeEq S m)
                            ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                              Algebra.TensorProduct.includeLeft),
                          (mapEquivMonic R S k : (a : MvPolynomial (Fin k) R →ₐ[R] S) → MonicDegreeEq S k)
                            ((↑f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S).comp
                              Algebra.TensorProduct.includeRight))
                        sorry :
                      { q : MonicDegreeEq S m × MonicDegreeEq S k // (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }))
                  ((fun
                        (q :
                          { q : MonicDegreeEq S m × MonicDegreeEq S k //
                            (↑q.1 : S[X]) * (↑q.2 : S[X]) = (↑p : S[X]) }) ↦
                      (Subtype.mk (p := fun (f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S) ↦
                          f.comp (universalFactorizationMap R n m k hn) =
                            (Equiv.symm (mapEquivMonic R S n) :
                                (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                              p)
                          (Algebra.TensorProduct.lift
                            ((Equiv.symm (mapEquivMonic R S m) :
                                (a : MonicDegreeEq S m) → MvPolynomial (Fin m) R →ₐ[R] S)
                              (↑q : MonicDegreeEq S m × MonicDegreeEq S k).1)
                            ((Equiv.symm (mapEquivMonic R S k) :
                                (a : MonicDegreeEq S k) → MvPolynomial (Fin k) R →ₐ[R] S)
                              (↑q : MonicDegreeEq S m × MonicDegreeEq S k).2)
                            sorry)
                          sorry :
                        { f : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R →ₐ[R] S //
                          f.comp (universalFactorizationMap R n m k hn) =
                            (Equiv.symm (mapEquivMonic R S n) :
                                (a : MonicDegreeEq S n) → MvPolynomial (Fin n) R →ₐ[R] S)
                              p }))
                    q)) :
              MonicDegreeEq S m × MonicDegreeEq S k).1 :
        S[X])
      n_1 =
    (↑(↑q : MonicDegreeEq S m × MonicDegreeEq S k).1 : S[X]).coeff n_1
Tactic: ext