awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
x : A
hx : IsIntegral R x
refine_2 :
  ∀ (y : R) (fx_eq : Eq.{u_3 + 1} (α := B) ((algebraMap R B : (a : R) → B) y : B) ((f : (a : A) → B) x : B)),
    ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
⊢ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
obtain ⟨y, fx_eq⟩ := cl.mp ((isIntegral_algHom_iff f hf).mpr hx)

Premises used: Iff.mpr, isIntegral_algHom_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
x : A
hx : IsIntegral R x
y : R
fx_eq : Eq.{u_3 + 1} (α := B) ((algebraMap R B : (a : R) → B) y : B) ((f : (a : A) → B) x : B)
⊢ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
aesop
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
y : R
refine_3 : IsIntegral.{u_1, u_3} R (A := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) y : A) : B)
⊢ IsIntegral.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) y : A)

Tactic:
apply (isIntegral_algHom_iff f hf).mp

Premises used: isIntegral_algHom_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
y : R
⊢ IsIntegral.{u_1, u_3} R (A := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) y : A) : B)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
⊢ IsIntegrallyClosedIn R A ↔ IsIntegrallyClosedIn R B

Tactic:
⟨AlgHom.isIntegrallyClosedIn e.symm e.symm.injective, AlgHom.isIntegrallyClosedIn e e.injective⟩

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, AlgHom.isIntegrallyClosedIn, Iff.intro, AlgEquiv.injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ IsIntegrallyClosed R ↔ IsIntegrallyClosedIn R K

Tactic:
(IsLocalization.algEquiv R⁰ _ _).isIntegrallyClosedIn

Premises used: nonZeroDivisors, AlgEquiv.isIntegrallyClosedIn, IsLocalization.algEquiv
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ IsIntegrallyClosed R ↔ IsIntegralClosure R R K

Tactic:
isIntegrallyClosed_iff_isIntegrallyClosedIn K

Premises used: isIntegrallyClosed_iff_isIntegrallyClosedIn
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  IsIntegrallyClosedIn R A →
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
      ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
mpr :
  (Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
      ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x) →
    IsIntegrallyClosedIn R A
⊢ IsIntegrallyClosedIn R A ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
      ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
constructor
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
algebraMap_injective : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
cl : ∀ {x : A}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
    ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
simp_all
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
cl : ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
x : A
⊢ IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
simp_all
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
cl : ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
mpr : ∀ {x : A}, (∃ (y : R), (algebraMap R A : (a : R) → A) y = x) → IsIntegral R x
⊢ IsIntegrallyClosedIn R A

Tactic:
refine ⟨inj, by simp_all, ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
cl : ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
y : R
⊢ IsIntegral.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) y : A)

Tactic:
apply isIntegral_algebraMap

Premises used: isIntegral_algebraMap
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ (y : R), (algebraMap R K : (a : R) → K) y = x

Tactic:
simp [isIntegrallyClosed_iff_isIntegrallyClosedIn K, isIntegrallyClosedIn_iff,
        IsFractionRing.injective R K]

Premises used: IsFractionRing.injective, isIntegrallyClosedIn_iff, isIntegrallyClosed_iff_isIntegrallyClosedIn
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
K : Type u_4
inst_5 : CommRing K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
⊢ IsIntegrallyClosedIn (↥(integralClosure R A)) A

Tactic:
isIntegrallyClosedIn_iff.mpr
    ⟨FaithfulSMul.algebraMap_injective _ _, fun h ↦ ⟨⟨_, isIntegral_trans _ h⟩, rfl⟩⟩

Premises used: Iff.mpr, isIntegral_trans, Subtype.mk, isIntegrallyClosedIn_iff, FaithfulSMul.algebraMap_injective, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
K : Type u_4
inst_5 : CommRing K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
⊢ IsIntegrallyClosedIn (↥(Subalgebra.toSubring (integralClosure R A))) A

Tactic:
inferInstanceAs (IsIntegrallyClosedIn (integralClosure R A) A)

Premises used: _private.0.instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure._proof_1
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
rw :
  (∀ {x : A}, IsIntegral (↥S) x → ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x) ↔
    ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
⊢ IsIntegrallyClosedIn (↥S) A ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
rw [isIntegrallyClosedIn_iff, and_iff_right (FaithfulSMul.algebraMap_injective _ _)]

Premises used: and_iff_right, isIntegrallyClosedIn_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x) ↔
    ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
congr(∀ _ _, _ ∈ $Subtype.range_val)

Premises used: congrArg, Membership.mem, id, Subtype, Subtype.range_val, IsIntegral, implies_congr, Eq.refl, pi_congr, iff_of_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x) ↔
    ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
exact congr(∀ _ _, _ ∈ $Subtype.range_val)
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
inst_3 : IsFractionRing (↥S) A
rw :
  (∀ {x : A}, IsIntegral (↥S) x → ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x) ↔
    ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
⊢ IsIntegrallyClosed.{u_2} ↥S ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
rw [isIntegrallyClosed_iff A]

Premises used: isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
inst_3 : IsFractionRing (↥S) A
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x) ↔
    ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
congr(∀ _ _, _ ∈ $Subtype.range_val)

Premises used: congrArg, Membership.mem, id, Subtype, Subtype.range_val, IsIntegral, implies_congr, Eq.refl, pi_congr, iff_of_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
inst_3 : IsFractionRing (↥S) A
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x) ↔
    ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
exact congr(∀ _ _, _ ∈ $Subtype.range_val)
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
T : Subring A
inst_3 : IsIntegrallyClosedIn (↥T) A
rw :
  (∀ (a : A) (b : a ∈ S),
      Membership.mem (α := A) T ((algebraMap (↥S) A : (a : ↥S) → A) (Subtype.mk (p := fun (a : A) ↦ a ∈ S) a b) : A)) ↔
    ∀ ⦃x : A⦄, Membership.mem (γ := Subring A) (ofClass S) x → x ∈ T
⊢ Subalgebra.toSubring (R := ↥S) (integralClosure (↥S) A) ≤ T ↔ ofClass S ≤ T

Tactic:
rw [integralClosure_le_iff, Subtype.forall, SetLike.le_def]

Premises used: SetLike.le_def, Subtype.forall, Subring.integralClosure_le_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
T : Subring A
inst_3 : IsIntegrallyClosedIn (↥T) A
⊢ (∀ (a : A) (b : a ∈ S),
      Membership.mem (α := A) T ((algebraMap (↥S) A : (a : ↥S) → A) (Subtype.mk (p := fun (a : A) ↦ a ∈ S) a b) : A)) ↔
    ∀ ⦃x : A⦄, Membership.mem (γ := Subring A) (ofClass S) x → x ∈ T

Tactic:
rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst_1 : CommRing R
inst_2 : CommRing A
inst_3 : Algebra R A
⊢ ∀ {x : R}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R R : (a : R) → R) y = x

Tactic:
simp [Algebra.IsIntegral.isIntegral]

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsIntegrallyClosedIn R A
x : A
⊢ IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
IsIntegralClosure.isIntegral_iff.mp

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsIntegrallyClosedIn R A
x : A
⊢ IsIntegral R x ↔ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
IsIntegralClosure.isIntegral_iff

Premises used: IsIntegralClosure.isIntegral_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsIntegrallyClosedIn R A
x : A
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
⊢ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
isIntegral_iff.mp <| hx.of_pow hn

Premises used: IsIntegrallyClosedIn.isIntegral_iff, IsIntegral.of_pow, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
S : Subalgebra R A
inst_3 : IsIntegrallyClosedIn (↥S) A
x : A
n : ℕ
hn : 0 < n
hx : x ^ n ∈ S
⊢ ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x

Tactic:
exists_algebraMap_eq_of_isIntegral_pow hn <| isIntegral_iff.mpr ⟨⟨x ^ n, hx⟩, rfl⟩

Premises used: Iff.mpr, IsIntegrallyClosedIn.isIntegral_iff, IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow, Subtype.mk, HPow.hPow, Exists.intro, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Eq (α := Subalgebra R A) (integralClosure R A) ⊥ ↔ IsIntegrallyClosedIn R A

Tactic:
eq_bot_iff.trans ?_

Premises used: Iff.trans, eq_bot_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
refine : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥ ↔ IsIntegrallyClosedIn R A
⊢ Eq (α := Subalgebra R A) (integralClosure R A) ⊥ ↔ IsIntegrallyClosedIn R A

Tactic:
refine eq_bot_iff.trans ?_

Premises used: Iff.trans, eq_bot_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
mp : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥ → IsIntegrallyClosedIn R A
mpr : IsIntegrallyClosedIn R A → LE.le (α := Subalgebra R A) (integralClosure R A) ⊥
⊢ LE.le (α := Subalgebra R A) (integralClosure R A) ⊥ ↔ IsIntegrallyClosedIn R A

Tactic:
constructor
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥
⊢ IsIntegrallyClosedIn R A

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

Premises used: Set.mem_range, Algebra.mem_bot, IsIntegralClosure.mk, Iff.intro, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥
mp : ∀ {x : A}, (∃ (y : R), (algebraMap R A : (a : R) → A) y = x) → IsIntegral R x
⊢ IsIntegrallyClosedIn R A

Tactic:
refine ⟨ hRA, fun hx => Set.mem_range.mp (Algebra.mem_bot.mp (h hx)), ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥
y : R
⊢ IsIntegral.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) y : A)

Tactic:
apply isIntegral_algebraMap

Premises used: isIntegral_algebraMap
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h : IsIntegrallyClosedIn R A
x : A
hx : Membership.mem (γ := Subalgebra R A) (integralClosure R A) x
mpr : ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
⊢ Membership.mem (γ := Subalgebra R A) ⊥ x

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

Premises used: Set.mem_range, Algebra.mem_bot
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h : IsIntegrallyClosedIn R A
x : A
hx : Membership.mem (γ := Subalgebra R A) (integralClosure R A) x
⊢ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
isIntegral_iff.mp hx

Premises used: IsIntegrallyClosedIn.isIntegral_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h : IsIntegrallyClosedIn R A
x : A
hx : Membership.mem (γ := Subalgebra R A) (integralClosure R A) x
⊢ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
exact isIntegral_iff.mp hx

Premises used: IsIntegrallyClosedIn.isIntegral_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsIntegrallyClosedIn R A
inst_4 : IsDomain R
inst_5 : Module.IsTorsionFree R A
inst_6 : Nontrivial A
⊢ Eq (α := Subalgebra R A) (integralClosure R A) ⊥

Tactic:
(integralClosure_eq_bot_iff A (FaithfulSMul.algebraMap_injective _ _)).mpr ‹_›

Premises used: Iff.mpr, IsIntegrallyClosedIn.integralClosure_eq_bot_iff, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : IsIntegralClosure A R B
⊢ IsIntegrallyClosedIn A B

Tactic:
have : Algebra.IsIntegral R A := IsIntegralClosure.isIntegral_algebra R B
  IsIntegralClosure.tower_top (R := R)

Premises used: IsIntegralClosure.isIntegral_algebra, IsIntegralClosure.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : IsIntegrallyClosedIn A B
inst_8 : Algebra.IsIntegral R A
⊢ IsIntegralClosure A R B

Tactic:
⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩

Premises used: IsIntegralClosure.isIntegral_iff, IsIntegralClosure.mk, IsIntegralClosure.algebraMap_injective, Iff.intro, Iff.mp, IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : IsIntegrallyClosedIn A B
inst_8 : Algebra.IsIntegral R A
refine : ∀ {x : B}, (∃ (y : A), (algebraMap A B : (a : A) → B) y = x) → IsIntegral R x
⊢ IsIntegralClosure A R B

Tactic:
refine ⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : IsIntegrallyClosedIn A B
inst_8 : Algebra.IsIntegral R A
y : A
⊢ IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) y : B)

Tactic:
IsIntegral.map (IsScalarTower.toAlgHom A A B) (Algebra.IsIntegral.isIntegral y)

Premises used: Algebra.IsIntegral.isIntegral, IsScalarTower.toAlgHom, IsIntegral.map
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : IsIntegrallyClosedIn A B
inst_8 : Algebra.IsIntegral R A
y : A
⊢ IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) y : B)

Tactic:
exact IsIntegral.map (IsScalarTower.toAlgHom A A B) (Algebra.IsIntegral.isIntegral y)

Premises used: Algebra.IsIntegral.isIntegral, IsScalarTower.toAlgHom, IsIntegral.map
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : CommRing K
inst_3 : Algebra R K
ifr : IsFractionRing R K
iic : IsIntegrallyClosed R
⊢ IsIntegralClosure R R K

Tactic:
(isIntegrallyClosed_iff_isIntegralClosure K).mp iic

Premises used: Iff.mp, isIntegrallyClosed_iff_isIntegralClosure
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : CommRing K
inst_2 : Algebra R K
ifr : IsFractionRing R K
inst_3 : IsIntegrallyClosed R
x : K
⊢ IsIntegral R x → ∃ (y : R), (algebraMap R K : (a : R) → K) y = x

Tactic:
IsIntegralClosure.isIntegral_iff.mp

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : CommRing K
inst_2 : Algebra R K
ifr : IsFractionRing R K
inst_3 : IsIntegrallyClosed R
x : K
⊢ IsIntegral R x ↔ ∃ (y : R), (algebraMap R K : (a : R) → K) y = x

Tactic:
IsIntegrallyClosedIn.isIntegral_iff

Premises used: IsIntegrallyClosedIn.isIntegral_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : CommRing K
inst_2 : Algebra R K
ifr : IsFractionRing R K
inst_3 : IsIntegrallyClosed R
x : K
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
⊢ ∃ (y : R), (algebraMap R K : (a : R) → K) y = x

Tactic:
IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow hn hx

Premises used: IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra R K
S : Subalgebra R K
inst_3 : IsIntegrallyClosed.{u_4} ↥S
inst_4 : IsFractionRing (↥S) K
x : K
n : ℕ
hn : 0 < n
hx : x ^ n ∈ S
⊢ ∃ (y : ↥S), (algebraMap (↥S) K : (a : ↥S) → K) y = x

Tactic:
IsIntegrallyClosedIn.exists_algebraMap_eq_of_pow_mem_subalgebra hn hx

Premises used: IsIntegrallyClosedIn.exists_algebraMap_eq_of_pow_mem_subalgebra