∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} [Nontrivial S] {p : Polynomial S},
  p ∈ Polynomial.lifts f → p.Monic → ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree ∧ q.Monic