no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : RatFunc K → Prop
x : RatFunc K
f : ∀ (p q : K[X]), q ≠ 0 → P (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q)
p q : K[X]
hq : q ≠ 0
⊢ P (RatFunc.mk p q)
simpa using f p q hq