R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
let e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ _ _
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ IsIntegrallyClosed R → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x

case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) → IsIntegrallyClosed R
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
constructor
case mp.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
⊢ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ IsIntegrallyClosed R → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
rintro ⟨cl⟩
case mp.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
x✝ : K
hx : IsIntegral R x✝
⊢ ∃ y, ↑(algebraMap R K) y = x✝
case mp.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
⊢ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
refine' fun hx => _
case mp.mk.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
x✝ : K
hx : IsIntegral R x✝
y : R
hy : ↑(algebraMap R (FractionRing R)) y = ↑e x✝
⊢ ∃ y, ↑(algebraMap R K) y = x✝
case mp.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
x✝ : K
hx : IsIntegral R x✝
⊢ ∃ y, ↑(algebraMap R K) y = x✝
obtain ⟨y, hy⟩ := cl ((isIntegral_algEquiv e).mpr hx)
no goals
case mp.mk.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
x✝ : K
hx : IsIntegral R x✝
y : R
hy : ↑(algebraMap R (FractionRing R)) y = ↑e x✝
⊢ ∃ y, ↑(algebraMap R K) y = x✝
exact ⟨y, e.algebraMap_eq_apply.mp hy⟩
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
⊢ IsIntegrallyClosed R
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) → IsIntegrallyClosed R
rintro cl
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : FractionRing R
hx : IsIntegral R x✝
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = x✝
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
⊢ IsIntegrallyClosed R
refine' ⟨fun hx => _⟩
case mpr.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : FractionRing R
hx : IsIntegral R x✝
y : R
hy : ↑(algebraMap R K) y = ↑(AlgEquiv.symm e) x✝
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = x✝
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : FractionRing R
hx : IsIntegral R x✝
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = x✝
obtain ⟨y, hy⟩ := cl ((isIntegral_algEquiv e.symm).mpr hx)
no goals
case mpr.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : FractionRing R
hx : IsIntegral R x✝
y : R
hy : ↑(algebraMap R K) y = ↑(AlgEquiv.symm e) x✝
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = x✝
exact ⟨y, e.symm.algebraMap_eq_apply.mp hy⟩