case pos
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)

case neg
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)
K : Type u
inst✝ : Field K
p q : K[X]
⊢ num (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) =
    ↑C (leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q)
by_cases hq : q = 0
no goals
case pos
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)
simp [hq]
no goals
case neg
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)
exact num_div' p hq