awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
S : Type u_4
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : Algebra S B
inst_9 : IsScalarTower R S B
inst_10 : Algebra R A
inst_11 : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x : S
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((lift R A B : (a : S) → A) x : A) : B)
    ((algebraMap S B : (a : S) → B) x : B)

Tactic:
algebraMap_mk' A (algebraMap S B x) (IsIntegral.algebraMap
    (Algebra.IsIntegral.isIntegral (R := R) x))

Premises used: Algebra.IsIntegral.isIntegral, Algebra.algebraMap, IsIntegralClosure.mk', IsIntegralClosure.algebraMap_mk', Classical.choose, IsIntegral.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
A' : Type u_4
inst_6 : CommRing A'
inst_7 : Algebra A' B
inst_8 : IsIntegralClosure A' R B
inst_9 : Algebra R A
inst_10 : Algebra R A'
inst_11 : IsScalarTower R A B
inst_12 : IsScalarTower R A' B
H :
  ∀ (x : A'),
    Eq (α := A') ((AlgHom.comp (lift R A' B) (lift R A B) : (a : A') → A') x : A')
      ((AlgHom.id R A' : (a : A') → A') x : A')
⊢ Eq (α := A' →ₐ[R] A') (AlgHom.comp (lift R A' B) (lift R A B)) (AlgHom.id R A')

Tactic:
ext x
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
A' : Type u_4
inst_6 : CommRing A'
inst_7 : Algebra A' B
inst_8 : IsIntegralClosure A' R B
inst_9 : Algebra R A
inst_10 : Algebra R A'
inst_11 : IsScalarTower R A B
inst_12 : IsScalarTower R A' B
x : A'
H :
  Eq.{u_3 + 1} (α := B)
    ((algebraMap A' B : (a : A') → B) ((AlgHom.comp (lift R A' B) (lift R A B) : (a : A') → A') x : A') : B)
    ((algebraMap A' B : (a : A') → B) ((AlgHom.id R A' : (a : A') → A') x : A') : B)
⊢ Eq (α := A') ((AlgHom.comp (lift R A' B) (lift R A B) : (a : A') → A') x : A')
    ((AlgHom.id R A' : (a : A') → A') x : A')

Tactic:
apply algebraMap_injective A' R B

Premises used: IsIntegralClosure.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
A' : Type u_4
inst_6 : CommRing A'
inst_7 : Algebra A' B
inst_8 : IsIntegralClosure A' R B
inst_9 : Algebra R A
inst_10 : Algebra R A'
inst_11 : IsScalarTower R A B
inst_12 : IsScalarTower R A' B
x : A'
⊢ Eq.{u_3 + 1} (α := B)
    ((algebraMap A' B : (a : A') → B) ((AlgHom.comp (lift R A' B) (lift R A B) : (a : A') → A') x : A') : B)
    ((algebraMap A' B : (a : A') → B) ((AlgHom.id R A' : (a : A') → A') x : A') : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
A' : Type u_4
inst_6 : CommRing A'
inst_7 : Algebra A' B
inst_8 : IsIntegralClosure A' R B
inst_9 : Algebra R A
inst_10 : Algebra R A'
inst_11 : IsScalarTower R A B
inst_12 : IsScalarTower R A' B
H :
  ∀ (x : A),
    Eq (α := A) ((AlgHom.comp (lift R A B) (lift R A' B) : (a : A) → A) x : A) ((AlgHom.id R A : (a : A) → A) x : A)
⊢ Eq (α := A →ₐ[R] A) (AlgHom.comp (lift R A B) (lift R A' B)) (AlgHom.id R A)

Tactic:
ext x
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
A' : Type u_4
inst_6 : CommRing A'
inst_7 : Algebra A' B
inst_8 : IsIntegralClosure A' R B
inst_9 : Algebra R A
inst_10 : Algebra R A'
inst_11 : IsScalarTower R A B
inst_12 : IsScalarTower R A' B
x : A
H :
  Eq.{u_3 + 1} (α := B)
    ((algebraMap A B : (a : A) → B) ((AlgHom.comp (lift R A B) (lift R A' B) : (a : A) → A) x : A) : B)
    ((algebraMap A B : (a : A) → B) ((AlgHom.id R A : (a : A) → A) x : A) : B)
⊢ Eq (α := A) ((AlgHom.comp (lift R A B) (lift R A' B) : (a : A) → A) x : A) ((AlgHom.id R A : (a : A) → A) x : A)

Tactic:
apply algebraMap_injective A R B

Premises used: IsIntegralClosure.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
A' : Type u_4
inst_6 : CommRing A'
inst_7 : Algebra A' B
inst_8 : IsIntegralClosure A' R B
inst_9 : Algebra R A
inst_10 : Algebra R A'
inst_11 : IsScalarTower R A B
inst_12 : IsScalarTower R A' B
x : A
⊢ Eq.{u_3 + 1} (α := B)
    ((algebraMap A B : (a : A) → B) ((AlgHom.comp (lift R A B) (lift R A' B) : (a : A) → A) x : A) : B)
    ((algebraMap A B : (a : A) → B) ((AlgHom.id R A : (a : A) → A) x : A) : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R B
inst_4 : Algebra A B
inst_5 : IsIntegralClosure A R B
A' : Type u_4
inst_6 : CommRing A'
inst_7 : Algebra A' B
inst_8 : IsIntegralClosure A' R B
inst_9 : Algebra R A
inst_10 : Algebra R A'
inst_11 : IsScalarTower R A B
inst_12 : IsScalarTower R A' B
x : A
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A' B : (a : A') → B) ((equiv R A B A' : (a : A) → A') x : A') : B)
    ((algebraMap A B : (a : A) → B) x : B)

Tactic:
algebraMap_lift R A' B (isIntegral := isIntegral_algebra R B) x

Premises used: IsIntegralClosure.algebraMap_lift, IsIntegralClosure.mk', Classical.choose
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
hx : IsIntegral A x
rcases : ∀ (p : A[X]) (pmonic : p.Monic) (hp : eval₂ (algebraMap A B) x p = 0), IsIntegral R x
⊢ IsIntegral R x

Tactic:
rcases hx with ⟨p, pmonic, hp⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
⊢ Module.Finite.{u_1, u_2} R ↥S

Tactic:
have : Module.Finite R S := ⟨(Subalgebra.toSubmodule S).fg_top.mpr <|
    fg_adjoin_of_finite p.coeffs.finite_toSet fun a _ ↦ Algebra.IsIntegral.isIntegral a⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
rw : eval₂ (algebraMap A B) x (Polynomial.map (algebraMap (↥S) A) p') = 0
⊢ eval₂ (algebraMap (↥S) B) x p' = 0

Tactic:
rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]

Premises used: Membership.mem, Subtype, Polynomial.eval₂_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ eval₂ (algebraMap A B) x p = 0

Tactic:
hp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
h : Polynomial.map (algebraMap (↥S) A) p' = p
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap (↥S) A) p') = 0

Tactic:
convert! hp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ Polynomial.map (algebraMap (↥S) A) p' = p

Tactic:
apply p.map_toSubring S.toSubring

Premises used: Subalgebra.toSubring, Polynomial.map_toSubring
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ IsIntegral.{u_2, u_3} (↥S) x

Tactic:
have hSx : IsIntegral S x := ⟨p', (p.monic_toSubring _ _).mpr pmonic, by
    rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]
    convert! hp; apply p.map_toSubring S.toSubring⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral.{u_2, u_3} (↥S) x
Sx : Submodule.{u_2, u_3} (↥S) B := (Subalgebra.toSubmodule : (a : Subalgebra (↥S) B) → Submodule (↥S) B) (↥S)[x]
MSx : Module.{u_2, u_3} ↥S ↥Sx := SMulMemClass.toModule Sx
⊢ Module.Finite.{u_2, u_3} ↥S ↥Sx

Tactic:
have : Module.Finite S Sx := .of_fg hSx.fg_adjoin_singleton
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this_1 : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral.{u_2, u_3} (↥S) x
Sx : Submodule.{u_2, u_3} (↥S) B := (Subalgebra.toSubmodule : (a : Subalgebra (↥S) B) → Submodule (↥S) B) (↥S)[x]
MSx : Module.{u_2, u_3} ↥S ↥Sx := SMulMemClass.toModule Sx
this : Module.Finite.{u_2, u_3} ↥S ↥Sx
⊢ IsIntegral R x

Tactic:
.of_mem_of_fg ((S[x]).restrictScalars R) ?_ _
    ((Subalgebra.mem_restrictScalars R).mpr <| subset_adjoin rfl)

Premises used: Subalgebra.mem_restrictScalars, Iff.mpr, Algebra.subset_adjoin, Algebra.adjoin, Membership.mem, Subtype, IsIntegral.of_mem_of_fg, Singleton.singleton, Subalgebra.restrictScalars, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this_1 : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral.{u_2, u_3} (↥S) x
Sx : Submodule.{u_2, u_3} (↥S) B := (Subalgebra.toSubmodule : (a : Subalgebra (↥S) B) → Submodule (↥S) B) (↥S)[x]
MSx : Module.{u_2, u_3} ↥S ↥Sx := SMulMemClass.toModule Sx
this : Module.Finite.{u_2, u_3} ↥S ↥Sx
refine :
  FG.{u_1, u_3} (R := R) (M := B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B)
      (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥S) (↥S)[x]))
⊢ IsIntegral R x

Tactic:
refine .of_mem_of_fg ((S[x]).restrictScalars R) ?_ _
    ((Subalgebra.mem_restrictScalars R).mpr <| subset_adjoin rfl)
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this_1 : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral.{u_2, u_3} (↥S) x
Sx : Submodule.{u_2, u_3} (↥S) B := (Subalgebra.toSubmodule : (a : Subalgebra (↥S) B) → Submodule (↥S) B) (↥S)[x]
MSx : Module.{u_2, u_3} ↥S ↥Sx := SMulMemClass.toModule Sx
this : Module.Finite.{u_2, u_3} ↥S ↥Sx
rw :
  Module.Finite.{u_1, u_3} R
    ↥((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B)
          (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥S) (↥S)[x]) :
        Submodule R B)
⊢ FG.{u_1, u_3} (R := R) (M := B)
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B)
      (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥S) (↥S)[x]))

Tactic:
rw [← Module.Finite.iff_fg]

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this_1 : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral.{u_2, u_3} (↥S) x
Sx : Submodule.{u_2, u_3} (↥S) B := (Subalgebra.toSubmodule : (a : Subalgebra (↥S) B) → Submodule (↥S) B) (↥S)[x]
MSx : Module.{u_2, u_3} ↥S ↥Sx := SMulMemClass.toModule Sx
this_2 : Module.Finite.{u_2, u_3} ↥S ↥Sx
this : SMul.{u_2, u_3} ↥S ↥Sx := @SemigroupAction.toSMul _ _ Monoid.toSemigroup _
⊢ IsScalarTower.{u_1, u_2, u_3} R ↥S ↥Sx

Tactic:
have : IsScalarTower R S Sx :=
    Submodule.isScalarTower Sx
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this_1 : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral.{u_2, u_3} (↥S) x
Sx : Submodule.{u_2, u_3} (↥S) B := (Subalgebra.toSubmodule : (a : Subalgebra (↥S) B) → Submodule (↥S) B) (↥S)[x]
MSx : Module.{u_2, u_3} ↥S ↥Sx := SMulMemClass.toModule Sx
this_2 : Module.Finite.{u_2, u_3} ↥S ↥Sx
this_3 : SMul.{u_2, u_3} ↥S ↥Sx := @SemigroupAction.toSMul _ _ Monoid.toSemigroup _
this : IsScalarTower.{u_1, u_2, u_3} R ↥S ↥Sx
⊢ Module.Finite.{u_1, u_3} R
    ↥((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B)
          (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥S) (↥S)[x]) :
        Submodule R B)

Tactic:
Module.Finite.trans S Sx

Premises used: Set.Mem, Membership.mem, Subtype, Module.Finite.trans
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R (↑p.coeffs : Set A)
this_1 : Module.Finite.{u_1, u_2} R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral.{u_2, u_3} (↥S) x
Sx : Submodule.{u_2, u_3} (↥S) B := (Subalgebra.toSubmodule : (a : Subalgebra (↥S) B) → Submodule (↥S) B) (↥S)[x]
MSx : Module.{u_2, u_3} ↥S ↥Sx := SMulMemClass.toModule Sx
this_2 : Module.Finite.{u_2, u_3} ↥S ↥Sx
this_3 : SMul.{u_2, u_3} ↥S ↥Sx := @SemigroupAction.toSMul _ _ Monoid.toSemigroup _
this : IsScalarTower.{u_1, u_2, u_3} R ↥S ↥Sx
⊢ Module.Finite.{u_1, u_3} R
    ↥((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B)
          (Subalgebra.restrictScalars.{u_1, u_2, u_3} R (S := ↥S) (↥S)[x]) :
        Submodule R B)

Tactic:
exact Module.Finite.trans S Sx

Premises used: Membership.mem, Subtype, Module.Finite.trans
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
inst_7 : Algebra.IsIntegral R A
inst_8 : Algebra.IsIntegral A B
⊢ Algebra.IsIntegral R B

Tactic:
⟨fun x ↦ isIntegral_trans x (Algebra.IsIntegral.isIntegral (R := A) x)⟩

Premises used: Algebra.IsIntegral.isIntegral, isIntegral_trans, Algebra.IsIntegral.mk
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsIntegral
hg : g.IsIntegral
⊢ (g.comp f).IsIntegral

Tactic:
let _ := f.toAlgebra; let _ := g.toAlgebra; let _ := (g.comp f).toAlgebra
  have : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  have : Algebra.IsIntegral R S := ⟨hf⟩
  have : Algebra.IsIntegral S T := ⟨hg⟩
  have : Algebra.IsIntegral R T := Algebra.IsIntegral.trans S
  Algebra.IsIntegral.isIntegral

Premises used: Algebra.IsIntegral.isIntegral, Algebra.IsIntegral.trans, RingHom.comp, IsIntegral, IsScalarTower.of_algebraMap_eq, RingHom.IsIntegral, Algebra.IsIntegral.mk, RingHom.toAlgebra, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
C : Type u_7
inst_3 : CommSemiring C
inst_4 : CommRing B
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : Algebra C B
inst_8 : IsScalarTower R A B
inst_9 : IsIntegralClosure C R B
inst_10 : Algebra.IsIntegral R A
⊢ IsIntegralClosure C A B

Tactic:
⟨IsIntegralClosure.algebraMap_injective _ R _,
   fun hx => (IsIntegralClosure.isIntegral_iff).mp (isIntegral_trans (R := R) _ hx),
   fun hx => ((IsIntegralClosure.isIntegral_iff (R := R)).mpr hx).tower_top⟩

Premises used: Iff.mpr, IsIntegralClosure.isIntegral_iff, IsIntegralClosure.mk, IsIntegralClosure.algebraMap_injective, isIntegral_trans, Iff.intro, Iff.mp, IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.IsIntegral

Tactic:
fun x ↦ (hf x).recOn fun _y hy ↦ hy ▸ f.isIntegralElem_map

Premises used: RingHom.IsIntegral, Exists.recOn
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra A B
inst_4 : Algebra R B
inst_5 : Algebra R A
inst_6 : IsScalarTower R A B
H : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
x : A
h : IsIntegral.{u_1, u_3} R (A := B) ((algebraMap A B : (a : A) → B) x : B)
⊢ IsIntegral R x

Tactic:
(isIntegral_algHom_iff (IsScalarTower.toAlgHom R A B) H).mp h

Premises used: IsScalarTower.toAlgHom, isIntegral_algHom_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Injective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
hfg : (g.comp f).IsIntegral
⊢ f.IsIntegral

Tactic:
letI := f.toAlgebra; letI := g.toAlgebra; letI := (g.comp f).toAlgebra
  haveI : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  fun x ↦ IsIntegral.tower_bot hg (hfg (g x))

Premises used: IsIntegral.tower_bot, IsIntegral, RingHom.IsIntegral, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsTorsionFree S T
inst_8 : Nontrivial T
inst_9 : IsScalarTower R S T
h : Algebra.IsIntegral R T
apply : RingHom.IsIntegral (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
⊢ ∀ (x : S), IsIntegral R x

Tactic:
apply RingHom.IsIntegral.tower_bot (algebraMap R S) (algebraMap S T)
      (FaithfulSMul.algebraMap_injective S T)

Premises used: RingHom.IsIntegral.tower_bot, Algebra.algebraMap, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsTorsionFree S T
inst_8 : Nontrivial T
inst_9 : IsScalarTower R S T
h : Algebra.IsIntegral R T
rw : RingHom.IsIntegral (algebraMap R T)
⊢ RingHom.IsIntegral (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))

Tactic:
rw [← IsScalarTower.algebraMap_eq R S T]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsTorsionFree S T
inst_8 : Nontrivial T
inst_9 : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ RingHom.IsIntegral (algebraMap R T)

Tactic:
h.isIntegral

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral, RingHom.IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsTorsionFree S T
inst_8 : Nontrivial T
inst_9 : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ RingHom.IsIntegral (algebraMap R T)

Tactic:
exact h.isIntegral

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommRing R
inst_1 : Field A
inst_2 : Ring B
inst_3 : Nontrivial B
inst_4 : Algebra R A
inst_5 : Algebra A B
inst_6 : Algebra R B
inst_7 : IsScalarTower R A B
x : A
h : IsIntegral.{u_6, u_8} R (A := B) ((algebraMap A B : (a : A) → B) x : B)
⊢ IsIntegral R x

Tactic:
h.tower_bot (algebraMap A B).injective

Premises used: Algebra.algebraMap, IsIntegral.tower_bot, RingHom.injective