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✝)
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
induction f using RatFunc.induction_on
no goals
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✝)
simp_rw [laurent_div, taylor_taylor]