-- Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean
theorem isIntegrallyClosedIn_iff {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] :
    IsIntegrallyClosedIn R A ↔
      Function.Injective (algebraMap R A) ∧
        ∀ {x : A}, IsIntegral R x → ∃ y, algebraMap R A y = x

Proof state:
case mpr.intro
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
x✝ : A
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝

Tactic:
rintro ⟨y, rfl⟩

Result:
case mpr.intro.intro
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
y : R
⊢ IsIntegral R ((algebraMap R A) y)

Proof state:
case mpr.intro
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
⊢ IsIntegrallyClosedIn R A

Tactic:
refine ⟨inj, by aesop, ?_⟩

Result:
case mpr.intro
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
x✝ : A
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝

Proof state:
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ IsIntegrallyClosedIn R A ↔
    Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

Tactic:
constructor

Result:
case mp
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ IsIntegrallyClosedIn R A →
    Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

case mpr
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x) →
    IsIntegrallyClosedIn R A

Proof state:
case mp.mk
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
algebraMap_injective'✝ : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x ↔ ∃ y, (algebraMap R A) y = x
⊢ Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

Tactic:
aesop

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
y : R
⊢ IsIntegral R ((algebraMap R A) y)

Tactic:
apply isIntegral_algebraMap

Result:
no goals

Proof state:
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
x✝ : A
⊢ IsIntegral R x✝ → ∃ y, (algebraMap R A) y = x✝

Tactic:
aesop

Result:
no goals

Proof state:
case mp
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ IsIntegrallyClosedIn R A →
    Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

Tactic:
rintro ⟨_, cl⟩

Result:
case mp.mk
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
algebraMap_injective'✝ : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x ↔ ∃ y, (algebraMap R A) y = x
⊢ Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

Proof state:
case mpr
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x) →
    IsIntegrallyClosedIn R A

Tactic:
rintro ⟨inj, cl⟩

Result:
case mpr.intro
R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
⊢ IsIntegrallyClosedIn R A