∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (x : Polynomial K) (y : ↥(nonZeroDivisors (Polynomial K))),
  { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) x y } = IsLocalization.mk' (RatFunc K) x y