no goals
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
⊢ ↑(liftMonoidWithZeroHom φ hφ) (↑(algebraMap K[X] (RatFunc K)) p) /
      ↑(liftMonoidWithZeroHom φ hφ) (↑(algebraMap K[X] (RatFunc K)) q) =
    ↑φ p / ↑φ q
rw [← map_div₀, liftMonoidWithZeroHom_apply_div]