∀ {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) (p : Polynomial.MonicDegreeEq R n) (q : { q // ↑q.1 * ↑q.2 = Polynomial.map (algebraMap R S) ↑p })
  (r : MvPolynomial (Fin n) R),
  ((↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm q)).comp
        (MvPolynomial.universalFactorizationMap R n m k hn))
      r =
    (algebraMap (MvPolynomial (Fin n) R) S) r