awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ Eq (α := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] ⊤
have h₁ : ∀ (g : S[X] ⧸ I),
  Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g ↔
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g ↔
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
have h₁ : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g →
  Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h₁ :
  Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g →
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g ↔
    Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
have h₂ : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g →
  Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g
have h₁ : ∀ (g' : S[X]) (hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g),
  Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g
Tactic: obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g
⊢ g = ((aeval ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X) : S[X] →ₐ[S] S[X] ⧸ I) : (a : S[X]) → S[X] ⧸ I) g'
have nth_rw : Eq.{u_4 + 1} (α := S[X] ⧸ I)
  (∑ x ∈ Finset.range (g'.natDegree + 1),
    (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I)
      (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (g'.coeff x) : S[X]) (HPow.hPow (α := S[X]) X x)))
  (∑ i ∈ Finset.range (g'.natDegree + 1),
    g'.coeff i • HPow.hPow (α := S[X] ⧸ I) ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I) i)
Tactic: nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
Goal:
S : Type u_4
inst : CommRing S
g_1 : S[X]
mon : g_1.Monic
I : Ideal S[X]
h : g_1 ∈ I
g : S[X] ⧸ I
h_1 : Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) ⊤ g
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) g' = g
⊢ Membership.mem (γ := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] g
have this : g = ((aeval ((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X) : S[X] →ₐ[S] S[X] ⧸ I) : (a : S[X]) → S[X] ⧸ I) g'
Tactic: have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
        nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
        simp only [Polynomial.C_mul', ← map_pow, map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
Goal:
S : Type u_4
inst : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ RingHom.IsIntegral (AlgHom.toRingHom (AlgHom.comp (Ideal.Quotient.mkₐ S I) (Algebra.ofId S S[X])))
have eq_top : Eq (α := Subalgebra S (S[X] ⧸ I)) S[((Ideal.Quotient.mkₐ S I : (a : S[X]) → S[X] ⧸ I) X : S[X] ⧸ I)] ⊤
Tactic: have eq_top : Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} = ⊤ := by
    ext g
    constructor
    · simp only [Algebra.mem_top, implies_true]
    · intro _
      obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g
      have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
        nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
        simp only [Polynomial.C_mul', ← map_pow, map_smul]
      exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
inst_6 : Module R A
inst_7 : IsScalarTower R A B
inst_8 : IsTorsionFree R B
⊢ IsTorsionFree R A
have _ : ∀ (x : R) (x_1 : A),
  (algebraMap A B : (a : A) → B) (x • x_1) = HSMul.hSMul (β := B) x ((algebraMap A B : (a : A) → B) x_1 : B)
Tactic: refine
    Function.Injective.moduleIsTorsionFree _ (IsIntegralClosure.algebraMap_injective A R B)
      fun _ _ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
h : IsIntegral.{u_1, u_3} R (A := B) 1
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A 1 h) : B) ((algebraMap A B : (a : A) → B) 1 : B)
have rw : Eq.{u_3 + 1} (α := B) (1 : B) ((algebraMap A B : (a : A) → B) 1 : B)
Tactic: rw [algebraMap_mk', map_one]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
h : IsIntegral.{u_1, u_3} R (A := B) 1
rw : Eq.{u_3 + 1} (α := B) (1 : B) ((algebraMap A B : (a : A) → B) 1 : B)
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A 1 h) : B) ((algebraMap A B : (a : A) → B) 1 : B)
have rw₁ : Eq.{u_3 + 1} (α := B) 1 1
Tactic: rw [algebraMap_mk', map_one]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
h : IsIntegral.{u_1, u_3} R (A := B) 0
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A 0 h) : B) ((algebraMap A B : (a : A) → B) 0 : B)
have rw : Eq.{u_3 + 1} (α := B) (0 : B) ((algebraMap A B : (a : A) → B) 0 : B)
Tactic: rw [algebraMap_mk', map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
h : IsIntegral.{u_1, u_3} R (A := B) 0
rw : Eq.{u_3 + 1} (α := B) (0 : B) ((algebraMap A B : (a : A) → B) 0 : B)
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A 0 h) : B) ((algebraMap A B : (a : A) → B) 0 : B)
have rw₁ : Eq.{u_3 + 1} (α := B) 0 0
Tactic: rw [algebraMap_mk', map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
inst_6 : Algebra R A
inst_7 : IsScalarTower R A B
x : R
h : IsIntegral.{u_1, u_3} R (A := B) ((algebraMap R B : (a : R) → B) x : B)
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A ((algebraMap R B : (a : R) → B) x) h) : B)
    ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A) : B)
have rw : Eq.{u_3 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B)
  ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A) : B)
Tactic: rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
inst_6 : Algebra R A
inst_7 : IsScalarTower R A B
x : R
h : IsIntegral.{u_1, u_3} R (A := B) ((algebraMap R B : (a : R) → B) x : B)
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B)
    ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A) : B)
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) (mk' A ((algebraMap R B : (a : R) → B) x) h) : B)
    ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A) : B)
have rw₁ : Eq.{u_3 + 1} (α := B) ((algebraMap R B : (a : R) → B) x : B) ((algebraMap R B : (a : R) → B) x : B)
Tactic: rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 y : S
⊢ mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) (x * y) : B) ⋯ =
    mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) x : B) ⋯ *
      mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) y : B) ⋯
have simp_rw : mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) (x * y) : B) sorry =
  mk'.{u_1, u_2, u_3} (R := R) A
    (HMul.hMul (α := B) (β := B) ((algebraMap S B : (a : S) → B) x : B) ((algebraMap S B : (a : S) → B) y : B)) sorry
Tactic: simp_rw [← mk'_mul, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 y : S
⊢ mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) (x + y) : B) ⋯ =
    mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) x : B) ⋯ +
      mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) y : B) ⋯
have simp_rw : mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) (x + y) : B) sorry =
  mk'.{u_1, u_2, u_3} (R := R) A
    (HAdd.hAdd (α := B) (β := B) ((algebraMap S B : (a : S) → B) x : B) ((algebraMap S B : (a : S) → B) y : B)) sorry
Tactic: simp_rw [← mk'_add, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 : R
⊢ mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) x : S) : B)
      ⋯ =
    (algebraMap R A : (a : R) → A) x
have simp_rw : mk'.{u_1, u_2, u_3} (R := R) A (B := B) ((algebraMap R B : (a : R) → B) x : B) sorry = (algebraMap R A : (a : R) → A) x
Tactic: simp_rw [← IsScalarTower.algebraMap_apply, mk'_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ Eq (α := A' →ₐ[R] A') (AlgHom.comp (lift R A' B) (lift R A B)) (AlgHom.id R A')
have 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')
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 (α := 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')
have 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)
Tactic: apply algebraMap_injective A' R B
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ Eq (α := A →ₐ[R] A) (AlgHom.comp (lift R A B) (lift R A' B)) (AlgHom.id R A)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 (α := 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)
have 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)
Tactic: apply algebraMap_injective A R B
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ IsIntegral R x
have rcases : ∀ (p : A[X]) (pmonic : p.Monic) (hp : eval₂ (algebraMap A B) x p = 0), IsIntegral R x
Tactic: rcases hx with ⟨p, pmonic, hp⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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)
⊢ IsIntegral R x
have this : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 (↥S) B) x p' = 0
have rw : eval₂ (algebraMap A B) x (Polynomial.map (algebraMap (↥S) A) p') = 0
Tactic: rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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 (Polynomial.map (algebraMap (↥S) A) p') = 0
have h : Polynomial.map (algebraMap (↥S) A) p' = p
Tactic: convert! hp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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 R x
have hSx : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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
⊢ IsIntegral R x
have this₁ : Module.Finite.{u_2, u_3} ↥S ↥Sx
Tactic: have : Module.Finite S Sx := .of_fg hSx.fg_adjoin_singleton
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
have 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]))
Tactic: refine .of_mem_of_fg ((S[x]).restrictScalars R) ?_ _
    ((Subalgebra.mem_restrictScalars R).mpr <| subset_adjoin rfl)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ 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]))
have 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)
Tactic: rw [← Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
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 _
⊢ 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)
have this₁ : IsScalarTower.{u_1, u_2, u_3} R ↥S ↥Sx
Tactic: have : IsScalarTower R S Sx :=
    Submodule.isScalarTower Sx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
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
⊢ ∀ (x : S), IsIntegral R x
have apply : RingHom.IsIntegral (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
Tactic: apply RingHom.IsIntegral.tower_bot (algebraMap R S) (algebraMap S T)
      (FaithfulSMul.algebraMap_injective S T)