case h
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : FractionRing K[X]
⊢ ↑(RingEquiv.symm (toFractionRingRingEquiv K)) x =
    ↑(AlgEquiv.toRingEquiv (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K))) x
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ RingEquiv.symm (toFractionRingRingEquiv K) =
    AlgEquiv.toRingEquiv (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K))
ext x
no goals
case h
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : FractionRing K[X]
⊢ ↑(RingEquiv.symm (toFractionRingRingEquiv K)) x =
    ↑(AlgEquiv.toRingEquiv (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K))) x
simp [toFractionRingRingEquiv, ofFractionRing_eq, AlgEquiv.coe_ringEquiv']