∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f f_1 : R →+* S) (e_f : f = f_1)
  (p : Polynomial R) (q : Polynomial S) (h : q ∣ Polynomial.map f p), AdjoinRoot.map f p q h = AdjoinRoot.map f_1 p q ⋯