[GOAL]
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]⁰
[PROOFSTEP]
rw [mem_nonZeroDivisors_iff]
[GOAL]
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
[PROOFSTEP]
intro x hx
[GOAL]
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
[PROOFSTEP]
have : x = taylor (r - r) x := by simp
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
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 
[GOAL]
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]⁰
[PROOFSTEP]
exact taylor_mem_nonZeroDivisors r
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ ↑(laurentAux r) (↑(algebraMap R[X] (RatFunc R)) p) = ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑(taylor r) p)
[PROOFSTEP]
rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one, map_one]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ ↑(laurent r) X = X + ↑C r
[PROOFSTEP]
rw [← algebraMap_X, laurent_algebraMap, taylor_X, _root_.map_add, algebraMap_C]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
x : R
⊢ ↑(laurent r) (↑C x) = ↑C x
[PROOFSTEP]
rw [← algebraMap_C, laurent_algebraMap, taylor_C]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ ↑(laurent 0) f = f
[PROOFSTEP]
induction f using RatFunc.induction_on
[GOAL]
case f
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
p✝ q✝ : R[X]
hq✝ : q✝ ≠ 0
⊢ ↑(laurent 0) (↑(algebraMap R[X] (RatFunc R)) p✝ / ↑(algebraMap R[X] (RatFunc R)) q✝) =
    ↑(algebraMap R[X] (RatFunc R)) p✝ / ↑(algebraMap R[X] (RatFunc R)) q✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ ↑(laurent r) (↑(laurent s) f) = ↑(laurent (r + s)) f
[PROOFSTEP]
induction f using RatFunc.induction_on
[GOAL]
case f
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
p✝ q✝ : R[X]
hq✝ : q✝ ≠ 0
⊢ ↑(laurent r) (↑(laurent s) (↑(algebraMap R[X] (RatFunc R)) p✝ / ↑(algebraMap R[X] (RatFunc R)) q✝)) =
    ↑(laurent (r + s)) (↑(algebraMap R[X] (RatFunc R)) p✝ / ↑(algebraMap R[X] (RatFunc R)) q✝)
[PROOFSTEP]
simp_rw [laurent_div, taylor_taylor]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f x✝¹ x✝ : RatFunc R
h : ↑(laurent r) x✝¹ = ↑(laurent r) x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa [laurent_laurent] using congr_arg (laurent (-r)) h
