awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f_1 : R ≃+* S
h : IsIntegrallyClosed R
x : Algebra S R := f_1.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv (f := f_1.symm) ⋯
g : AlgEquiv.{u_2, u_2, u_1} S (FractionRing S) (FractionRing R) := IsFractionRing.algEquivOfAlgEquiv f
⊢ IsIntegrallyClosed S

Tactic:
(isIntegrallyClosed_iff (FractionRing S)).mpr (fun hx ↦ ?_)

Premises used: Iff.mpr, FractionRing, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f_1 : R ≃+* S
h : IsIntegrallyClosed R
x : Algebra S R := f_1.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv (f := f_1.symm) ⋯
g : AlgEquiv.{u_2, u_2, u_1} S (FractionRing S) (FractionRing R) := IsFractionRing.algEquivOfAlgEquiv f
refine :
  ∀ {x : FractionRing S} (hx : IsIntegral S x),
    ∃ (y : S), (algebraMap S (FractionRing S) : (a : S) → FractionRing S) y = x
⊢ IsIntegrallyClosed S

Tactic:
refine (isIntegrallyClosed_iff (FractionRing S)).mpr (fun hx ↦ ?_)

Premises used: Iff.mpr, FractionRing, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f_1 : R ≃+* S
h : IsIntegrallyClosed R
x : Algebra S R := f_1.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv (f := f_1.symm) ⋯
g : AlgEquiv.{u_2, u_2, u_1} S (FractionRing S) (FractionRing R) := IsFractionRing.algEquivOfAlgEquiv f
x_1 : FractionRing S
hx : IsIntegral S x_1
rcases :
  ∀ (z : R)
    (hz :
      Eq (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) z : FractionRing R)
        ((g : (a : FractionRing S) → FractionRing R) x_1 : FractionRing R)),
    ∃ (y : S), (algebraMap S (FractionRing S) : (a : S) → FractionRing S) y = x_1
⊢ ∃ (y : S), (algebraMap S (FractionRing S) : (a : S) → FractionRing S) y = x_1

Tactic:
rcases (isIntegrallyClosed_iff _).mp h ((isIntegral_algEquiv g).mpr hx).tower_top with ⟨z, hz⟩

Premises used: Iff.mpr, isIntegral_algEquiv, Iff.mp, isIntegrallyClosed_iff, IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f_1 : R ≃+* S
h : IsIntegrallyClosed R
x : Algebra S R := f_1.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv (f := f_1.symm) ⋯
g : AlgEquiv.{u_2, u_2, u_1} S (FractionRing S) (FractionRing R) := IsFractionRing.algEquivOfAlgEquiv f
x_1 : FractionRing S
hx : IsIntegral S x_1
z : R
hz :
  Eq (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) z : FractionRing R)
    ((g : (a : FractionRing S) → FractionRing R) x_1 : FractionRing R)
⊢ ∃ (y : S), (algebraMap S (FractionRing S) : (a : S) → FractionRing S) y = x_1

Tactic:
⟨f.symm z, (IsFractionRing.algEquivOfAlgEquiv_algebraMap f.symm z).symm.trans <|
    (AlgEquiv.symm_apply_eq g).mpr hz⟩

Premises used: Iff.mpr, AlgEquiv.symm_apply_eq, AlgEquiv.symm, IsFractionRing.algEquivOfAlgEquiv_algebraMap, Exists.intro, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f_1 : R ≃+* S
h : IsIntegrallyClosed R
x : Algebra S R := f_1.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv (f := f_1.symm) ⋯
g : AlgEquiv.{u_2, u_2, u_1} S (FractionRing S) (FractionRing R) := IsFractionRing.algEquivOfAlgEquiv f
x_1 : FractionRing S
hx : IsIntegral S x_1
z : R
hz :
  Eq (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) z : FractionRing R)
    ((g : (a : FractionRing S) → FractionRing R) x_1 : FractionRing R)
⊢ ∃ (y : S), (algebraMap S (FractionRing S) : (a : S) → FractionRing S) y = x_1

Tactic:
exact ⟨f.symm z, (IsFractionRing.algEquivOfAlgEquiv_algebraMap f.symm z).symm.trans <|
    (AlgEquiv.symm_apply_eq g).mpr hz⟩
-- 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
inst_4 : IsIntegrallyClosed R
inst_5 : Algebra S R
inst_6 : Algebra S K
inst_7 : IsScalarTower S R K
inst_8 : Algebra.IsIntegral S R
⊢ IsIntegralClosure R S K

Tactic:
IsIntegralClosure.of_isIntegrallyClosedIn

Premises used: IsIntegralClosure.of_isIntegrallyClosedIn
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
inst_4 : IsIntegrallyClosedIn R K
⊢ IsDomain R

Tactic:
have : IsDomain R := (FaithfulSMul.algebraMap_injective R K).isDomain _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
inst_4 : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K :=
  IsFractionRing.liftAlgHom.{u_4, u_4, u_4, u_5} (R := R) (A := R) (K := FractionRing R) (L := K) (g :=
    Algebra.ofId R K) ⋯
rw :
  ∀ {x : FractionRing R}, IsIntegral R x → ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = x
⊢ IsIntegrallyClosed R

Tactic:
rw [isIntegrallyClosed_iff (K := FractionRing R)]

Premises used: FractionRing, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
inst_4 : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K :=
  IsFractionRing.liftAlgHom.{u_4, u_4, u_4, u_5} (R := R) (A := R) (K := FractionRing R) (L := K) (g :=
    Algebra.ofId R K) ⋯
x : FractionRing R
hx : IsIntegral R x
⊢ ∃ (y : R), Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) ((f : (a : FractionRing R) → K) x : K)

Tactic:
(IsIntegralClosure.isIntegral_iff (A := R)).mp (hx.map f)

Premises used: IsIntegralClosure.isIntegral_iff, IsIntegral.map, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
inst_4 : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K :=
  IsFractionRing.liftAlgHom.{u_4, u_4, u_4, u_5} (R := R) (A := R) (K := FractionRing R) (L := K) (g :=
    Algebra.ofId R K) ⋯
x : FractionRing R
hx : IsIntegral R x
h :
  ∀ (x_1 : R),
    (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x_1 = x ↔
      Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x_1 : K) ((f : (a : FractionRing R) → K) x : K)
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = x

Tactic:
convert! (IsIntegralClosure.isIntegral_iff (A := R)).mp (hx.map f)

Premises used: IsIntegralClosure.isIntegral_iff, IsIntegral.map, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
inst_4 : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K :=
  IsFractionRing.liftAlgHom.{u_4, u_4, u_4, u_5} (R := R) (A := R) (K := FractionRing R) (L := K) (g :=
    Algebra.ofId R K) ⋯
x : FractionRing R
hx : IsIntegral R x
x_1 : R
⊢ (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x_1 = x ↔
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x_1 : K) ((f : (a : FractionRing R) → K) x : K)

Tactic:
simp [← f.toRingHom.injective.eq_iff]

Premises used: Function.Injective.eq_iff, RingHom.injective, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
⊢ IsIntegralClosure S R U

Tactic:
⟨?_, ?_⟩

Premises used: IsIntegralClosure.mk
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
refine_1 : Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U) (⇑(algebraMap S U) : (a : S) → U)
refine_2 : ∀ {x : U}, IsIntegral R x ↔ ∃ (y : S), (algebraMap S U : (a : S) → U) y = x
⊢ IsIntegralClosure S R U

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
refine_1 :
  Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T U) (algebraMap S T)) : (a : S) → U)
⊢ Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U) (⇑(algebraMap S U) : (a : S) → U)

Tactic:
rw [IsScalarTower.algebraMap_eq S T U]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
⊢ Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T U) (algebraMap S T)) : (a : S) → U)

Tactic:
(IsIntegralClosure.algebraMap_injective T T U).comp
      (IsIntegralClosure.algebraMap_injective S R T)

Premises used: IsIntegralClosure.algebraMap_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
⊢ Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T U) (algebraMap S T)) : (a : S) → U)

Tactic:
exact (IsIntegralClosure.algebraMap_injective T T U).comp
      (IsIntegralClosure.algebraMap_injective S R T)

Premises used: IsIntegralClosure.algebraMap_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : U
⊢ IsIntegral R x ↔ ∃ (y : S), (algebraMap S U : (a : S) → U) y = x

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : U
refine_2 : ∀ (h : IsIntegral R x), ∃ (y : S), (algebraMap S U : (a : S) → U) y = x
refine_2₁ : (∃ (y : S), (algebraMap S U : (a : S) → U) y = x) → IsIntegral R x
⊢ IsIntegral R x ↔ ∃ (y : S), (algebraMap S U : (a : S) → U) y = x

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : U
h : IsIntegral R x
refine_2 :
  ∀ (x : T) (h : IsIntegral.{u_4, u_7} R (A := U) ((algebraMap T U : (a : T) → U) x : U)),
    ∃ (y : S), Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U) ((algebraMap T U : (a : T) → U) x : U)
⊢ ∃ (y : S), (algebraMap S U : (a : S) → U) y = x

Tactic:
obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := T) (A := T)).mp h.tower_top

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp, IsIntegral.tower_top, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : T
h : IsIntegral.{u_4, u_7} R (A := U) ((algebraMap T U : (a : T) → U) x : U)
⊢ IsIntegral R x

Tactic:
rw [isIntegral_algebraMap_iff (IsIntegralClosure.algebraMap_injective T T U)] at h

Premises used: IsIntegralClosure.algebraMap_injective, isIntegral_algebraMap_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : T
h : IsIntegral R x
refine_2 :
  ∀ (x : S) (h : IsIntegral.{u_4, u_6} R (A := T) ((algebraMap S T : (a : S) → T) x : T)),
    ∃ (y : S),
      Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U)
        ((algebraMap T U : (a : T) → U) ((algebraMap S T : (a : S) → T) x : T) : U)
⊢ ∃ (y : S), Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U) ((algebraMap T U : (a : T) → U) x : U)

Tactic:
obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := R) (A := S)).mp h

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : S
h : IsIntegral.{u_4, u_6} R (A := T) ((algebraMap S T : (a : S) → T) x : T)
⊢ ∃ (y : S),
    Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U)
      ((algebraMap T U : (a : T) → U) ((algebraMap S T : (a : S) → T) x : T) : U)

Tactic:
⟨x, IsScalarTower.algebraMap_apply ..⟩

Premises used: Exists.intro, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : S
h : IsIntegral.{u_4, u_6} R (A := T) ((algebraMap S T : (a : S) → T) x : T)
⊢ ∃ (y : S),
    Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U)
      ((algebraMap T U : (a : T) → U) ((algebraMap S T : (a : S) → T) x : T) : U)

Tactic:
exact ⟨x, IsScalarTower.algebraMap_apply ..⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : S
refine_2 : IsIntegral.{u_4, u_7} R (A := U) ((algebraMap T U : (a : T) → U) ((algebraMap S T : (a : S) → T) x : T) : U)
⊢ IsIntegral.{u_4, u_7} R (A := U) ((algebraMap S U : (a : S) → U) x : U)

Tactic:
rw [IsScalarTower.algebraMap_apply S T U]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : S
⊢ IsIntegral.{u_4, u_7} R (A := U) ((algebraMap T U : (a : T) → U) ((algebraMap S T : (a : S) → T) x : T) : U)

Tactic:
((IsIntegralClosure.isIntegral_iff (A := S) (R := R) (B := T)).mpr ⟨x, rfl⟩).map
        (IsScalarTower.toAlgHom R T U)

Premises used: Iff.mpr, IsScalarTower.toAlgHom, IsIntegralClosure.isIntegral_iff, IsIntegral.map, Exists.intro, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : S
⊢ IsIntegral.{u_4, u_7} R (A := U) ((algebraMap T U : (a : T) → U) ((algebraMap S T : (a : S) → T) x : T) : U)

Tactic:
exact ((IsIntegralClosure.isIntegral_iff (A := S) (R := R) (B := T)).mpr ⟨x, rfl⟩).map
        (IsScalarTower.toAlgHom R T U)

Premises used: Iff.mpr, IsScalarTower.toAlgHom, IsIntegralClosure.isIntegral_iff, IsIntegral.map, Exists.intro, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : IsIntegrallyClosed S
inst_6 : IsIntegrallyClosedIn R S
⊢ IsIntegrallyClosed R

Tactic:
have : IsIntegrallyClosedIn R (FractionRing S) :=
    .of_isIntegralClosure_of_isIntegrallyClosedIn _ _ S _
  .of_isIntegrallyClosedIn R (FractionRing S)

Premises used: FractionRing, IsIntegralClosure.of_isIntegralClosure_of_isIntegrallyClosedIn, IsIntegrallyClosed.of_isIntegrallyClosedIn
-- 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
⊢ Eq (α := Subalgebra R K) (integralClosure R K) ⊥ ↔ IsIntegrallyClosed R

Tactic:
(IsIntegrallyClosedIn.integralClosure_eq_bot_iff _ (IsFractionRing.injective _ _)).trans
    (isIntegrallyClosed_iff_isIntegrallyClosedIn _).symm

Premises used: IsFractionRing.injective, IsIntegrallyClosedIn.integralClosure_eq_bot_iff, isIntegrallyClosed_iff_isIntegrallyClosedIn, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
⟨fun ⟨x, hx⟩ ↦ ?_, fun h ↦ pow_dvd_pow_of_dvd h n⟩

Premises used: Dvd.dvd, pow_dvd_pow_of_dvd, _private.0.IsIntegrallyClosed.pow_dvd_pow_iff.match_1, Iff.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
refine : a ^ n ∣ b ^ n → ∀ (x : R) (hx : b ^ n = a ^ n * x), a ∣ b
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
refine ⟨fun ⟨x, hx⟩ ↦ ?_, fun h ↦ pow_dvd_pow_of_dvd h n⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
pos : ∀ (ha : a = 0), a ∣ b
neg : ∀ (ha : ¬a = 0), a ∣ b
⊢ a ∣ b

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
ha : a = 0
⊢ a ∣ b

Tactic:
simpa [ha, hn] using hx
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
ha : ¬a = 0
K : Type u_1 := FractionRing R
⊢ Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)

Tactic:
replace ha : algebraMap R K a ≠ 0 := fun h ↦
    ha <| (injective_iff_map_eq_zero _).1 (IsFractionRing.injective R K) _ h
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
⊢ IsIntegral R y

Tactic:
⟨X ^ n - C x, monic_X_pow_sub_C _ hn, ?_⟩

Premises used: Polynomial.C, Polynomial.monic_X_pow_sub_C, HSub.hSub, RingHom.IsIntegralElem, IsIntegral, HPow.hPow, And.intro, Exists.intro, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
refine :
  eval₂ (algebraMap R K) y (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])) = 0
⊢ IsIntegral R y

Tactic:
refine ⟨X ^ n - C x, monic_X_pow_sub_C _ hn, ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
simp :
  HSub.hSub (β := K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) b : K) n /
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) a : K) n)
      (((algebraMap R K : R →+* K) : (a : R) → K) x : K) =
    0
⊢ eval₂ (algebraMap R K) y (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])) = 0

Tactic:
simp only [y, eval₂_sub, eval₂_X_pow, div_pow, eval₂_C]

Premises used: Polynomial.eval₂_X_pow, Polynomial.eval₂_sub, div_pow, Polynomial.eval₂_C