∀ (K : Type u_1) [inst : CommRing K] [inst_1 : IsDomain K] (R : Type u_2) [inst_2 : CommSemiring R]
  [inst_3 : Algebra R (Polynomial K)] (r : R),
  (RatFunc.toFractionRingRingEquiv K).toFun ((algebraMap R (RatFunc K)) r) =
    (algebraMap R (FractionRing (Polynomial K))) r