∀ {K : Type u} [inst : Field K] {R : Type u_1} {F : Type u_2} [inst_1 : CommRing R] [inst_2 : IsDomain R]
  [inst_3 : FunLike F (Polynomial K) (Polynomial R)] [inst_4 : MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (f : RatFunc K),
  (RatFunc.map φ hφ) f =
    (algebraMap (Polynomial R) (RatFunc R)) (φ f.num) / (algebraMap (Polynomial R) (RatFunc R)) (φ f.denom)