∀ {R : Type u} [inst : CommRing R] (r : R) (p : Polynomial R) [inst_1 : IsDomain R],
  (RatFunc.laurent r) ((algebraMap (Polynomial R) (RatFunc R)) p) =
    (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p)