rfl
case intro.mk.intro
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
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x
no goals