no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
y : { x // x ∈ K[X]⁰ }
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } = IsLocalization.mk' (RatFunc K) x y
rw [IsFractionRing.mk'_eq_div, IsFractionRing.mk'_eq_div, ← mk_eq_div', ← mk_eq_div]