-- Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean
theorem integralClosure_eq_bot_iff (hRA : Function.Injective (algebraMap R A)) :
    integralClosure R A = ⊥ ↔ IsIntegrallyClosedIn R A

Proof state:
case mp
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : integralClosure R A ≤ ⊥
x✝ : A
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝

Tactic:
rintro ⟨y, rfl⟩

Result:
case mp.intro
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : integralClosure R A ≤ ⊥
y : R
⊢ IsIntegral R ((algebraMap R A) y)

Proof state:
case mp.intro
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : integralClosure R A ≤ ⊥
y : R
⊢ IsIntegral R ((algebraMap R A) y)

Tactic:
apply isIntegral_algebraMap

Result:
no goals

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ x ∈ ⊥

Tactic:
rw [Algebra.mem_bot, Set.mem_range]

Result:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ ∃ y, (algebraMap R A) y = x

Proof state:
case mp
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
⊢ integralClosure R A ≤ ⊥ → IsIntegrallyClosedIn R A

Tactic:
intro h

Result:
case mp
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : integralClosure R A ≤ ⊥
⊢ IsIntegrallyClosedIn R A

Proof state:
case mp
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : integralClosure R A ≤ ⊥
⊢ IsIntegrallyClosedIn R A

Tactic:
refine ⟨ hRA, fun hx => Set.mem_range.mp (Algebra.mem_bot.mp (h hx)), ?_⟩

Result:
case mp
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : integralClosure R A ≤ ⊥
x✝ : A
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ ∃ y, (algebraMap R A) y = x

Tactic:
exact isIntegral_iff.mp hx

Result:
no goals

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
⊢ IsIntegrallyClosedIn R A → integralClosure R A ≤ ⊥

Tactic:
intro h x hx

Result:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ x ∈ ⊥

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
⊢ integralClosure R A = ⊥ ↔ IsIntegrallyClosedIn R A

Tactic:
refine eq_bot_iff.trans ?_

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
⊢ integralClosure R A ≤ ⊥ ↔ IsIntegrallyClosedIn R A

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
⊢ integralClosure R A ≤ ⊥ ↔ IsIntegrallyClosedIn R A

Tactic:
constructor

Result:
case mp
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
⊢ integralClosure R A ≤ ⊥ → IsIntegrallyClosedIn R A

case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
⊢ IsIntegrallyClosedIn R A → integralClosure R A ≤ ⊥