no goals
K F : Type u
inst✝ : Field F
p q : F[X]
f g : RatFunc F
⊢ ↑(algebraMap (RatFunc F) (LaurentSeries F)) (↑(algebraMap F[X] (RatFunc F)) p / ↑(algebraMap F[X] (RatFunc F)) q) =
    ↑(algebraMap F[X] (LaurentSeries F)) p / ↑(algebraMap F[X] (LaurentSeries F)) q
convert coe_div (algebraMap F[X] (RatFunc F) p) (algebraMap F[X] (RatFunc F) q) <;>
  rw [← mk_one, coe_def, coeAlgHom, mk_eq_div, liftAlgHom_apply_div, map_one, div_one,
    Algebra.ofId_apply]