awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
h : Nontrivial R
p :
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))[X]
hp : p.Monic
q : R[X] :=
  ∑ i ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : R[X])
      (HPow.hPow (α := R[X]) X i)
hq : q.natDegree = p.natDegree
e :
  Eq.{u_2 + 1} (α := S)
    (∑ b ∈ Finset.range (p.natDegree + 1),
      (HMul.hMul (α := S[X])
            ((algebraMap
                    (↥(Algebra.adjoin R
                        {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
                    S[X] :
                  (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
                (p.coeff b) :
              S[X])
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X ^ b)).coeff
        p.natDegree)
    0
⊢ Eq.{u_2 + 1} (α := S)
    (∑ x_1 ∈ Finset.range (p.natDegree + 1),
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((↑(p.coeff x_1) : R[X]).coeff (p.natDegree - x_1)) : S)
        (x ^ x_1))
    0
have inr : ∀ (i : ℕ) (hi : i ∈ Finset.range (p.natDegree + 1)),
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : S) (x ^ i) =
    (HMul.hMul (α := S[X])
          ((algebraMap
                  (↥(Algebra.adjoin R
                      {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
                  S[X] :
                (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
              (p.coeff i) :
            S[X])
          (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X ^ i)).coeff
      p.natDegree
Tactic: refine (Finset.sum_congr rfl fun i hi ↦ ?_).trans e
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
h : Nontrivial R
p :
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))[X]
hp : p.Monic
q : R[X] :=
  ∑ i ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : R[X])
      (HPow.hPow (α := R[X]) X i)
hq : q.natDegree = p.natDegree
e :
  Eq.{u_2 + 1} (α := S)
    (∑ b ∈ Finset.range (p.natDegree + 1),
      (HMul.hMul (α := S[X])
            ((algebraMap
                    (↥(Algebra.adjoin R
                        {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
                    S[X] :
                  (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
                (p.coeff b) :
              S[X])
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X ^ b)).coeff
        p.natDegree)
    0
i : ℕ
hi : i ∈ Finset.range (p.natDegree + 1)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : S) (x ^ i) =
    (HMul.hMul (α := S[X])
          ((algebraMap
                  (↥(Algebra.adjoin R
                      {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
                  S[X] :
                (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
              (p.coeff i) :
            S[X])
          (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X ^ i)).coeff
      p.natDegree
have hi₁ : i ≤ p.natDegree
Tactic: simp only [Finset.mem_range, Nat.lt_succ_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
h : Nontrivial R
p :
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))[X]
hp : p.Monic
q : R[X] :=
  ∑ i ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : R[X])
      (HPow.hPow (α := R[X]) X i)
hq : q.natDegree = p.natDegree
e :
  Eq.{u_2 + 1} (α := S)
    (∑ b ∈ Finset.range (p.natDegree + 1),
      (HMul.hMul (α := S[X])
            ((algebraMap
                    (↥(Algebra.adjoin R
                        {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
                    S[X] :
                  (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
                (p.coeff b) :
              S[X])
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X ^ b)).coeff
        p.natDegree)
    0
i : ℕ
hi : i ≤ p.natDegree
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : S) (x ^ i) =
    (HMul.hMul (α := S[X])
          ((algebraMap
                  (↥(Algebra.adjoin R
                      {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
                  S[X] :
                (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
              (p.coeff i) :
            S[X])
          (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X ^ i)).coeff
      p.natDegree
have inr : HMul.hMul (β := S) (x ^ i) ((algebraMap R S : (a : R) → S) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : S) =
  x ^ i *
    coeff
      ((algebraMap
            (↥(Algebra.adjoin R
                {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
            S[X] :
          (a : ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, (C : (a : R) → R[X]) r * X = x})) → S[X])
        (p.coeff i))
      (p.natDegree - i)
Tactic: rw [mul_pow, mul_left_comm, ← map_pow, coeff_C_mul, coeff_mul_X_pow', if_pos hi, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
x : S
h : Nontrivial R
p :
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))[X]
hp : p.Monic
e :
  eval₂
      (algebraMap
        (↥(Algebra.adjoin R
            {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
        S[X])
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X) p =
    0
q : R[X] :=
  ∑ i ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑(p.coeff i) : R[X]).coeff (p.natDegree - i)) : R[X])
      (HPow.hPow (α := R[X]) X i)
hq : q.natDegree = p.natDegree
⊢ ∀ (i : ℕ), q.coeff i ∈ I ^ (q.natDegree - i)
have inr : ∀ (i : ℕ), q.coeff i ∈ I ^ (p.natDegree - i)
Tactic: rw [hq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
have refine : IsIntegral.{u_1, u_2}
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
  (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
Tactic: refine exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral ?_
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
x : S
h : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)) x
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
have mem : ∀ (x : R) (hx : x ∈ (↑I : Set R)),
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap R S : (a : R) → S) x) : S[X]) X)
Tactic: obtain ⟨x, hx, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
a x : S
hx_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (a • x) : S[X]) X)
have smul : IsIntegral.{u_1, u_2}
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
  (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) a : S[X])
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X))
Tactic: simp only [smul_eq_mul, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x_1 : S
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
a x : S
hx_1 : Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x
hx :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) a : S[X])
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X))
have smul : IsIntegral.{u_1, u_2}
  ↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x})
  (A := S[X]) ((C : (a : S) → S[X]) a : S[X])
Tactic: refine .mul ?_ hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
have zero : IsIntegral.{u_1, u_2}
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
  (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) 0) X)
Tactic: induction hx using Submodule.span_induction with
  | zero => simp [isIntegral_zero]
  | add x y _ _ hx hy => simpa [add_mul] using hx.add hy
  | mem x h =>
    obtain ⟨x, hx, rfl⟩ := h
    simpa using isIntegral_algebraMap (R := A) (A := S[X])
      (x := ⟨C x * X, Algebra.subset_adjoin ⟨x, hx, rfl⟩⟩)
  | smul a x _ hx =>
    simp only [smul_eq_mul, map_mul, mul_assoc]
    refine .mul ?_ hx
    exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
zero :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) 0) X)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
have add : ∀ (x y : S),
  Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x →
    Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) y →
      ∀
        (hx :
          IsIntegral.{u_1, u_2}
            (↥(Algebra.adjoin R
                {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X))
        (hy :
          IsIntegral.{u_1, u_2}
            (↥(Algebra.adjoin R
                {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) y : S[X]) X)),
        IsIntegral.{u_1, u_2}
          (↥(Algebra.adjoin R
              {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
          (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (x + y) : S[X]) X)
Tactic: induction hx using Submodule.span_induction with
  | zero => simp [isIntegral_zero]
  | add x y _ _ hx hy => simpa [add_mul] using hx.add hy
  | mem x h =>
    obtain ⟨x, hx, rfl⟩ := h
    simpa using isIntegral_algebraMap (R := A) (A := S[X])
      (x := ⟨C x * X, Algebra.subset_adjoin ⟨x, hx, rfl⟩⟩)
  | smul a x _ hx =>
    simp only [smul_eq_mul, map_mul, mul_assoc]
    refine .mul ?_ hx
    exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
zero :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) 0) X)
add :
  ∀ (x y : S),
    Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x →
      Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) y →
        ∀
          (hx :
            IsIntegral.{u_1, u_2}
              (↥(Algebra.adjoin R
                  {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
              (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X))
          (hy :
            IsIntegral.{u_1, u_2}
              (↥(Algebra.adjoin R
                  {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
              (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) y : S[X]) X)),
          IsIntegral.{u_1, u_2}
            (↥(Algebra.adjoin R
                {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (x + y) : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
have mem : ∀ (x : S) (h : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)) x),
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
Tactic: induction hx using Submodule.span_induction with
  | zero => simp [isIntegral_zero]
  | add x y _ _ hx hy => simpa [add_mul] using hx.add hy
  | mem x h =>
    obtain ⟨x, hx, rfl⟩ := h
    simpa using isIntegral_algebraMap (R := A) (A := S[X])
      (x := ⟨C x * X, Algebra.subset_adjoin ⟨x, hx, rfl⟩⟩)
  | smul a x _ hx =>
    simp only [smul_eq_mul, map_mul, mul_assoc]
    refine .mul ?_ hx
    exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
let let₁ let₂ let₃ :
  ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
have let₄ : IsIntegral.{u_1, u_2}
  (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
  (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
Tactic: classical
  let A : Subalgebra R R[X] := Algebra.adjoin R { C r * X | r ∈ I }
  letI := Polynomial.algebra R S
  refine exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral ?_
  induction hx using Submodule.span_induction with
  | zero => simp [isIntegral_zero]
  | add x y _ _ hx hy => simpa [add_mul] using hx.add hy
  | mem x h =>
    obtain ⟨x, hx, rfl⟩ := h
    simpa using isIntegral_algebraMap (R := A) (A := S[X])
      (x := ⟨C x * X, Algebra.subset_adjoin ⟨x, hx, rfl⟩⟩)
  | smul a x _ hx =>
    simp only [smul_eq_mul, map_mul, mul_assoc]
    refine .mul ?_ hx
    exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I
have obtain : ∀ (p : R[X]) (hp : p.Monic) (e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S))
  (h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)),
  ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I
Tactic: obtain ⟨p, hp, e, h⟩ := exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I
have refine : ∀ (i : ℕ) (hi : i ≠ p.natDegree), p.coeff i ∈ I
Tactic: refine ⟨p, hp, e, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi : i ≠ p.natDegree
⊢ p.coeff i ∈ I
have inl : ∀ (hi : i < p.natDegree), p.coeff i ∈ I
Tactic: obtain hi | hi := hi.lt_or_gt
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
p : R[X]
hp : p.Monic
e : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
h : ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
i : ℕ
hi : i ≠ p.natDegree
inl : ∀ (hi : i < p.natDegree), p.coeff i ∈ I
⊢ p.coeff i ∈ I
have inr : ∀ (hi : p.natDegree < i), p.coeff i ∈ I
Tactic: obtain hi | hi := hi.lt_or_gt
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x})) (q.coeff i)
have rw : ∀ ⦃I : Ideal R⦄,
  Membership.mem (γ := Set (Ideal R))
      {J : Ideal R | Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ J ∧ J.IsPrime} I →
    q.coeff i ∈ I
Tactic: rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
⊢ map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree
have a : ∀ (i : ℕ), (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
Tactic: ext i