no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : RatFunc K → Prop
x : FractionRing K[X]
f : ∀ (p q : K[X]), q ≠ 0 → P (RatFunc.mk p q)
x✝ : K[X] × { x // x ∈ K[X]⁰ }
p : K[X]
q : { x // x ∈ K[X]⁰ }
⊢ P { toFractionRing := Localization.mk (p, q).fst (p, q).snd }
simpa only [mk_coe_def, Localization.mk_eq_mk'] using
  f p q (mem_nonZeroDivisors_iff_ne_zero.mp q.2)