no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
⊢ RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q
rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff,
  IsLocalization.mk'_eq_iff_eq', (IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]