case hq
K : Type u
inst✝³ : Field K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : RatFunc K
⊢ denom f ≠ 0
K : Type u
inst✝³ : Field K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : RatFunc K
⊢ ↑(map φ hφ) f =
    ↑(algebraMap ((fun x => R[X]) (num f)) (RatFunc R)) (↑φ (num f)) /
      ↑(algebraMap ((fun x => R[X]) (denom f)) (RatFunc R)) (↑φ (denom f))
rw [← num_div_denom f, map_apply_div_ne_zero, num_div_denom f]
no goals
case hq
K : Type u
inst✝³ : Field K
R : Type u_1
F : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : RatFunc K
⊢ denom f ≠ 0
exact denom_ne_zero _