no goals
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
f : RatFunc K
⊢ ↑(liftMonoidWithZeroHom φ hφ) f = ↑φ (num f) / ↑φ (denom f)
rw [← num_div_denom f, liftMonoidWithZeroHom_apply_div, num_div_denom]