no goals
K : Type u
inst✝ : Field K
p : K[X]
⊢ intDegree (↑(algebraMap K[X] (RatFunc K)) p) = ↑(natDegree p)
rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
  Int.ofNat_zero, sub_zero]