refine (isIntegrallyClosed_iff_isIntegralClosure (K := K)).mpr
  ⟨IsFractionRing.injective _ _, fun {x} ↦ ⟨?_, fun e ↦ e.choose_spec ▸ isIntegral_algebraMap⟩⟩
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
⊢ IsIntegrallyClosed S
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
⊢ IsIntegral S x → ∃ y, (algebraMap S K) y = x