no goals
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    ↑C (leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q)
rw [num, numDenom_div _ hq]