no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
⊢ RatFunc.mk p q =
    { toFractionRing := ↑(algebraMap K[X] (FractionRing K[X])) p / ↑(algebraMap K[X] (FractionRing K[X])) q }
rw [RatFunc.mk]