no goals
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)
rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one,
  map_one]