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
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) → IsIntegralClosure R R K

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
⊢ IsIntegralClosure R R K → ∀ {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
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) ↔ IsIntegralClosure R R K
constructor
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
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
⊢ IsIntegralClosure R R K
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
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) → IsIntegralClosure R R K
intro cl
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
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
⊢ (∃ y, ↑(algebraMap R K) y = x✝) → IsIntegral R 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
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
⊢ IsIntegralClosure R R K
refine' ⟨IsFractionRing.injective R K, ⟨cl, _⟩⟩
case mp.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
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
y : R
y_eq : ↑(algebraMap R K) y = x✝
⊢ IsIntegral R 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
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
⊢ (∃ y, ↑(algebraMap R K) y = x✝) → IsIntegral R x✝
rintro ⟨y, y_eq⟩
case mp.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
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
y : R
y_eq : ↑(algebraMap R K) y = x✝
⊢ IsIntegral R (↑(algebraMap R K) y)
case mp.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
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
y : R
y_eq : ↑(algebraMap R K) y = x✝
⊢ IsIntegral R x✝
rw [← y_eq]
no goals
case mp.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
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
y : R
y_eq : ↑(algebraMap R K) y = x✝
⊢ IsIntegral R (↑(algebraMap R K) y)
exact isIntegral_algebraMap
case mpr.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
cl : ∀ {x : K}, IsIntegral R x ↔ ∃ y, ↑(algebraMap R K) y = x
x : K
hx : 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
⊢ IsIntegralClosure R R K → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
rintro ⟨-, cl⟩ x hx
no goals
case mpr.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
cl : ∀ {x : K}, IsIntegral R x ↔ ∃ y, ↑(algebraMap R K) y = x
x : K
hx : IsIntegral R x
⊢ ∃ y, ↑(algebraMap R K) y = x
exact cl.mp hx