R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
⊢ ∀ (x : (fun x => R[X]) p), x * ↑(taylor r) p = 0 → x = 0
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
⊢ ↑(taylor r) p ∈ R[X]⁰
rw [mem_nonZeroDivisors_iff]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
x : R[X]
hx : x * ↑(taylor r) p = 0
⊢ x = 0
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
⊢ ∀ (x : (fun x => R[X]) p), x * ↑(taylor r) p = 0 → x = 0
intro x hx
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
x : R[X]
hx : x * ↑(taylor r) p = 0
this : x = ↑(taylor (r - r)) x
⊢ x = 0
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
x : R[X]
hx : x * ↑(taylor r) p = 0
⊢ x = 0
have : x = taylor (r - r) x := by simp
no goals
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
x : R[X]
hx : x * ↑(taylor r) p = 0
this : x = ↑(taylor (r - r)) x
⊢ x = 0
rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
  LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
  LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
no goals
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
x : R[X]
hx : x * ↑(taylor r) p = 0
⊢ x = ↑(taylor (r - r)) x
simp