no goals
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ R[X]⁰ ≤
    Submonoid.comap
      {
        toMonoidHom :=
          { toOneHom := { toFun := ↑(taylor r), map_one' := (_ : ↑(taylor r) 1 = ↑Polynomial.C 1) },
            map_mul' := (_ : ∀ (p q : R[X]), ↑(taylor r) (p * q) = ↑(taylor r) p * ↑(taylor r) q) },
        map_zero' := (_ : ↑(taylor r) 0 = 0),
        map_add' := (_ : ∀ (x y : R[X]), ↑(taylor r) (x + y) = ↑(taylor r) x + ↑(taylor r) y) }
      R[X]⁰
exact taylor_mem_nonZeroDivisors r