K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x✝¹ : RatFunc K
x✝ : FractionRing K[X]
x : K[X] × { x // x ∈ K[X]⁰ }
⊢ IsLocalization.mk' (Localization K[X]⁰) x.fst x.snd =
    IsLocalization.mk' (FractionRing K[X]) (↑(RingHom.id K[X]) x.fst)
      { val := ↑(RingHom.id K[X]) ↑x.snd, property := (_ : ↑x.snd ∈ Submonoid.comap (RingHom.id K[X]) K[X]⁰) }
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x✝¹ : RatFunc K
x✝ : FractionRing K[X]
x : K[X] × { x // x ∈ K[X]⁰ }
⊢ { toFractionRing := Localization.mk x.fst x.snd }.toFractionRing =
    ↑(IsLocalization.algEquiv K[X]⁰ (RatFunc K) (FractionRing K[X])) { toFractionRing := Localization.mk x.fst x.snd }
simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
  IsLocalization.ringEquivOfRingEquiv_apply, IsLocalization.map_mk',
  RingEquiv.coe_toRingHom, RingEquiv.refl_apply, SetLike.eta]
no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x✝¹ : RatFunc K
x✝ : FractionRing K[X]
x : K[X] × { x // x ∈ K[X]⁰ }
⊢ IsLocalization.mk' (Localization K[X]⁰) x.fst x.snd =
    IsLocalization.mk' (FractionRing K[X]) (↑(RingHom.id K[X]) x.fst)
      { val := ↑(RingHom.id K[X]) ↑x.snd, property := (_ : ↑x.snd ∈ Submonoid.comap (RingHom.id K[X]) K[X]⁰) }
simp only [IsFractionRing.mk'_eq_div, RingHom.id_apply, Subtype.coe_eta]