awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := 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}) x
hy_1 :
  Membership.mem (γ := 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}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
⊢ ∑ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, x.coeff x_1.1 * y.coeff x_1.2 ∈ I ^ i
have mul : ∀ (x_1 : ℕ × ℕ) (j₁ j₂ : ℕ) (hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i),
  x.coeff (j₁, j₂).1 * y.coeff (j₁, j₂).2 ∈ I ^ i
Tactic: refine sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := 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}) x
hy_1 :
  Membership.mem (γ := 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}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
x_1 : ℕ × ℕ
j₁ j₂ : ℕ
hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ x.coeff (j₁, j₂).1 * y.coeff (j₁, j₂).2 ∈ I ^ i
have mul : ∀ (hj : (j₁, j₂) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (j₁ + j₂)),
  x.coeff (j₁, j₂).1 * y.coeff (j₁, j₂).2 ∈ I ^ (j₁ + j₂)
Tactic: obtain rfl : j₁ + j₂ = i := by simpa using hj
Cleared hypotheses: i, hj
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P : R[X]
hP :
  Membership.mem (γ := 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}) P
i : ℕ
⊢ P.coeff i ∈ I ^ i
have mem : ∀ (x : R[X])
  (hx :
    Membership.mem (γ := Set R[X])
      {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x} x)
  (i : ℕ), x.coeff i ∈ I ^ i
Tactic: induction hP using Algebra.adjoin_induction generalizing i with
  | mem x hx =>
    obtain ⟨r, hrI, rfl⟩ := hx
    simp +contextual [coeff_X, apply_ite, hrI, @eq_comm _ 1]
  | algebraMap r => simp +contextual [coeff_C, apply_ite]
  | add x y hx hy _ _ => aesop
  | mul x y _ _ hx hy =>
    rw [coeff_mul]
    refine sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_
    obtain rfl : j₁ + j₂ = i := by simpa using hj
    exact pow_add I j₁ j₂ ▸ Ideal.mul_mem_mul (hx _) (hy _)
Cleared hypotheses: hP, i
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P : R[X]
hP :
  Membership.mem (γ := 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}) P
i : ℕ
mem :
  ∀ (x : R[X])
    (hx :
      Membership.mem (γ := Set R[X])
        {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x} x)
    (i : ℕ), x.coeff i ∈ I ^ i
⊢ P.coeff i ∈ I ^ i
have algebraMap : ∀ (r : R) (i : ℕ), coeff ((algebraMap R R[X] : (a : R) → R[X]) r) i ∈ I ^ i
Tactic: induction hP using Algebra.adjoin_induction generalizing i with
  | mem x hx =>
    obtain ⟨r, hrI, rfl⟩ := hx
    simp +contextual [coeff_X, apply_ite, hrI, @eq_comm _ 1]
  | algebraMap r => simp +contextual [coeff_C, apply_ite]
  | add x y hx hy _ _ => aesop
  | mul x y _ _ hx hy =>
    rw [coeff_mul]
    refine sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_
    obtain rfl : j₁ + j₂ = i := by simpa using hj
    exact pow_add I j₁ j₂ ▸ Ideal.mul_mem_mul (hx _) (hy _)
Cleared hypotheses: hP, i
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P : R[X]
hP :
  Membership.mem (γ := 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}) P
i : ℕ
mem :
  ∀ (x : R[X])
    (hx :
      Membership.mem (γ := Set R[X])
        {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x} x)
    (i : ℕ), x.coeff i ∈ I ^ i
algebraMap : ∀ (r : R) (i : ℕ), coeff ((Algebra.algebraMap R R[X] : (a : R) → R[X]) r) i ∈ I ^ i
⊢ P.coeff i ∈ I ^ i
have add : ∀ (x y : R[X])
  (hx :
    Membership.mem (γ := 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})
      x)
  (hy :
    Membership.mem (γ := 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})
      y),
  (∀ (i : ℕ), x.coeff i ∈ I ^ i) → (∀ (i : ℕ), y.coeff i ∈ I ^ i) → ∀ (i : ℕ), (x + y).coeff i ∈ I ^ i
Tactic: induction hP using Algebra.adjoin_induction generalizing i with
  | mem x hx =>
    obtain ⟨r, hrI, rfl⟩ := hx
    simp +contextual [coeff_X, apply_ite, hrI, @eq_comm _ 1]
  | algebraMap r => simp +contextual [coeff_C, apply_ite]
  | add x y hx hy _ _ => aesop
  | mul x y _ _ hx hy =>
    rw [coeff_mul]
    refine sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_
    obtain rfl : j₁ + j₂ = i := by simpa using hj
    exact pow_add I j₁ j₂ ▸ Ideal.mul_mem_mul (hx _) (hy _)
Cleared hypotheses: hP, i
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P : R[X]
hP :
  Membership.mem (γ := 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}) P
i : ℕ
mem :
  ∀ (x : R[X])
    (hx :
      Membership.mem (γ := Set R[X])
        {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x} x)
    (i : ℕ), x.coeff i ∈ I ^ i
algebraMap : ∀ (r : R) (i : ℕ), coeff ((Algebra.algebraMap R R[X] : (a : R) → R[X]) r) i ∈ I ^ i
add :
  ∀ (x y : R[X])
    (hx :
      Membership.mem (γ := 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})
        x)
    (hy :
      Membership.mem (γ := 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})
        y),
    (∀ (i : ℕ), x.coeff i ∈ I ^ i) → (∀ (i : ℕ), y.coeff i ∈ I ^ i) → ∀ (i : ℕ), (x + y).coeff i ∈ I ^ i
⊢ P.coeff i ∈ I ^ i
have mul : ∀ (x y : R[X]),
  Membership.mem (γ := 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})
      x →
    Membership.mem (γ := 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})
        y →
      ∀ (hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i) (hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i) (i : ℕ), (x * y).coeff i ∈ I ^ i
Tactic: induction hP using Algebra.adjoin_induction generalizing i with
  | mem x hx =>
    obtain ⟨r, hrI, rfl⟩ := hx
    simp +contextual [coeff_X, apply_ite, hrI, @eq_comm _ 1]
  | algebraMap r => simp +contextual [coeff_C, apply_ite]
  | add x y hx hy _ _ => aesop
  | mul x y _ _ hx hy =>
    rw [coeff_mul]
    refine sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_
    obtain rfl : j₁ + j₂ = i := by simpa using hj
    exact pow_add I j₁ j₂ ▸ Ideal.mul_mem_mul (hx _) (hy _)
Cleared hypotheses: hP, i
-- 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
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)
⊢ ∃ (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 inl : Subsingleton R →
  ∃ (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)
Tactic: cases subsingleton_or_nontrivial R
-- 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
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)
inl :
  Subsingleton R →
    ∃ (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 inr : Nontrivial R →
  ∃ (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)
Tactic: cases subsingleton_or_nontrivial R
-- 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
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)
h : Subsingleton R
⊢ ∃ (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 h : Monic.{u_1} (R := R) 0 ∧
  Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) 0 : S) (0 : S) ∧
    ∀ (i : ℕ), coeff 0 i ∈ I ^ (natDegree.{u_1} (R := R) 0 - i)
Tactic: use 0
-- 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
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)
h : Nontrivial R
⊢ ∃ (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 inr : ∀
  (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),
  ∃ (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)
Tactic: obtain ⟨p, hp, e⟩ := hx
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
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)
⊢ q.natDegree = p.natDegree
have refine_1 : ∀ 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)).natDegree ≤
    p.natDegree
Tactic: refine natDegree_eq_of_le_of_coeff_ne_zero (natDegree_sum_le_of_forall_le _ _ ?_) ?_
-- 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)
refine_1 :
  ∀ 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)).natDegree ≤
      p.natDegree
⊢ q.natDegree = p.natDegree
have refine_2 : q.coeff p.natDegree ≠ 0
Tactic: refine natDegree_eq_of_le_of_coeff_ne_zero (natDegree_sum_le_of_forall_le _ _ ?_) ?_
-- 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
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)
⊢ ∃ (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 hq : q.natDegree = p.natDegree
Tactic: have hq : q.natDegree = p.natDegree := by
    refine natDegree_eq_of_le_of_coeff_ne_zero (natDegree_sum_le_of_forall_le _ _ ?_) ?_
    · exact fun i hi ↦ (natDegree_C_mul_X_pow_le _ _).trans (by simpa [Nat.lt_succ_iff] using hi)
    · simp [q, hp]
-- 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
⊢ ∃ (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 inr : q.Monic
Tactic: refine ⟨q, ?_, ?_, ?_⟩
-- 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
inr : q.Monic
⊢ ∃ (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 inr₁ : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
Tactic: refine ⟨q, ?_, ?_, ?_⟩
-- 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
inr : q.Monic
inr₁ : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : 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 inr₂ : ∀ (i : ℕ), q.coeff i ∈ I ^ (q.natDegree - i)
Tactic: refine ⟨q, ?_, ?_, ?_⟩
-- 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
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
⊢ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
have 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).coeff
    p.natDegree =
  coeff 0 p.natDegree
Tactic: replace e := congr(($e).coeff p.natDegree)
Cleared hypotheses: 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 :
  (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).coeff
      p.natDegree =
    coeff 0 p.natDegree
⊢ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
have 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
Tactic: simp only [eval₂_eq_sum_range, finsetSum_coeff, coeff_zero] at e
Cleared hypotheses: e
-- 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) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
have inr : 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
Tactic: simp only [q, map_sum, map_mul, aeval_C, map_pow, aeval_X]