awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * p
q : R[X][X]
hq :
  HSub.hSub (β := R[X][X]) P ((C : (a : R[X]) → R[X][X]) (eval b P) : R[X][X]) =
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q
rw :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      q * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
    P
⊢ HMul.hMul (α := R[X][X]) (β := R[X][X]) ((C : (a : R[X]) → R[X][X]) p : R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X]) +
      q * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
    P
have rw₁ : HMul.hMul (α := R[X][X]) (β := R[X][X])
      ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
      ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
  P
Tactic: rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * p
q : R[X][X]
hq :
  HSub.hSub (β := R[X][X]) P ((C : (a : R[X]) → R[X][X]) (eval b P) : R[X][X]) =
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q
rw :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      q * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
    P
rw₁ :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
    P
⊢ HMul.hMul (α := R[X][X]) (β := R[X][X]) ((C : (a : R[X]) → R[X][X]) p : R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X]) +
      q * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
    P
have rw₂ : HMul.hMul (α := R[X][X]) (β := R[X][X])
      ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
      ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
  HAdd.hAdd (α := R[X][X]) ((C : (a : R[X]) → R[X][X]) (eval b P) : R[X][X])
    (HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q)
Tactic: rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * p
q : R[X][X]
hq :
  HSub.hSub (β := R[X][X]) P ((C : (a : R[X]) → R[X][X]) (eval b P) : R[X][X]) =
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q
rw :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      q * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
    P
rw₁ :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
    P
rw₂ :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
    HAdd.hAdd (α := R[X][X]) ((C : (a : R[X]) → R[X][X]) (eval b P) : R[X][X])
      (HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q)
⊢ HMul.hMul (α := R[X][X]) (β := R[X][X]) ((C : (a : R[X]) → R[X][X]) p : R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X]) +
      q * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
    P
have rw₃ : HMul.hMul (α := R[X][X]) (β := R[X][X])
      ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
      ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
  HAdd.hAdd (α := R[X][X])
    ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * p) : R[X][X])
    (HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q)
Tactic: rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * p
q : R[X][X]
hq :
  HSub.hSub (β := R[X][X]) P ((C : (a : R[X]) → R[X][X]) (eval b P) : R[X][X]) =
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q
rw :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      q * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
    P
rw₁ :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
    P
rw₂ :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
    HAdd.hAdd (α := R[X][X]) ((C : (a : R[X]) → R[X][X]) (eval b P) : R[X][X])
      (HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q)
rw₃ :
  HMul.hMul (α := R[X][X]) (β := R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
        ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
      HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
    HAdd.hAdd (α := R[X][X])
      ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * p) : R[X][X])
      (HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q)
⊢ HMul.hMul (α := R[X][X]) (β := R[X][X]) ((C : (a : R[X]) → R[X][X]) p : R[X][X])
        ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X]) +
      q * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
    P
have rw₄ : HMul.hMul (α := R[X][X]) (β := R[X][X])
      ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
      ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q =
  HMul.hMul (α := R[X][X]) (β := R[X][X])
      ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
      ((C : (a : R[X]) → R[X][X]) p : R[X][X]) +
    HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q
Tactic: rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
⊢ Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →+* R) (evalRingHom x))
    (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])})
have h : ∀ (y : R[X]),
  Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →+* R) (evalRingHom x)) y ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])})
      y
Tactic: ext y
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →+* R) constantCoeff) (Ideal.span {X})
have refine : ∀ (p : R[X]) (hp : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (F := R[X] →+* R) constantCoeff) p),
  Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span {X}) p
Tactic: refine le_antisymm (fun p hp ↦ ?_) (by simp [Ideal.span_le])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
hp : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (F := R[X] →+* R) constantCoeff) p
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span {X}) p
have hp₁ : X ∣ p
Tactic: simp only [RingHom.mem_ker, constantCoeff_apply, ← Polynomial.X_dvd_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y ↔
    ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
have mp : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y →
  ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
mp :
  Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y →
    ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y ↔
    ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
have mpr : (∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)) →
  Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y a : ↥R[x]
ha : Membership.mem (γ := Set ↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R)) a
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S)
have mp : ∀ (a : R) (ha : a ∈ (↑I : Set R)),
  ∃ (p : R[X]),
    (∀ (i : ℕ), p.coeff i ∈ I) ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) ((↑((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a) : S) : S)
Tactic: obtain ⟨a, ha, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
a : R
ha : a ∈ (↑I : Set R)
i : ℕ
⊢ coeff ((C : (a : R) → R[X]) a) i ∈ I
have rw : (if i = 0 then a else 0) ∈ I
Tactic: rw [coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y a b : ↥R[x]
ha :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) a
hb :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b
ha' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S)
hb' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑b : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a + b) : S)
have mp : ∀ (a_1 : R[X]) (ha : ∀ (i : ℕ), a_1.coeff i ∈ I) (ha' : (aeval x : (a : R[X]) → S) a_1 = (↑a : S)),
  ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a + b) : S)
Tactic: obtain ⟨a, ha, ha'⟩ := ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y a_1 b : ↥R[x]
ha_1 :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) a_1
hb :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b
hb' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑b : S)
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x : (a : R[X]) → S) a = (↑a_1 : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a_1 + b) : S)
have mp : ∀ (b_1 : R[X]) (hb : ∀ (i : ℕ), b_1.coeff i ∈ I) (hb' : (aeval x : (a : R[X]) → S) b_1 = (↑b : S)),
  ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a_1 + b) : S)
Tactic: obtain ⟨b, hb, hb'⟩ := hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y a b : ↥R[x]
hb :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b
hb' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑b : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a • b) : S)
have mp : ∀ (b' : R[X]) (hb : ∀ (i : ℕ), b'.coeff i ∈ I) (hb' : (aeval x : (a : R[X]) → S) b' = (↑b : S)),
  ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a • b) : S)
Tactic: obtain ⟨b', hb, hb'⟩ := hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y a b : ↥R[x]
hb_1 :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x : (a : R[X]) → S) b' = (↑b : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a • b) : S)
have mp : ∀ (p : R[X]) (hp : (aeval x : (a : R[X]) → S) p = (↑a : S)),
  ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a • b) : S)
Tactic: have ⟨p, hp⟩ := adjoin_eq_exists_aeval R x a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y a b : ↥R[x]
hb_1 :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x : (a : R[X]) → S) b' = (↑b : S)
p : R[X]
hp : (aeval x : (a : R[X]) → S) p = (↑a : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a • b) : S)
have mp : ∀ (i : ℕ), (p * b').coeff i ∈ I
Tactic: refine ⟨p * b', fun i ↦ ?_, by simp [hp, hb']⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y a b : ↥R[x]
hb_1 :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x : (a : R[X]) → S) b' = (↑b : S)
p : R[X]
hp : (aeval x : (a : R[X]) → S) p = (↑a : S)
i : ℕ
⊢ (p * b').coeff i ∈ I
have mp : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ i, p.coeff x.1 * b'.coeff x.2 ∈ I
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
H : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
have mp : ∀ (a : ↥R[x]) (ha : Membership.mem (γ := Set ↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R)) a),
  ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S)
Tactic: induction H using Submodule.span_induction with
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      exact ⟨C a, fun i ↦ by rw [coeff_C]; aesop, aeval_C _ _⟩
    | zero => exact ⟨0, by simp, aeval_zero _⟩
    | add a b ha hb ha' hb' =>
      obtain ⟨a, ha, ha'⟩ := ha'
      obtain ⟨b, hb, hb'⟩ := hb'
      exact ⟨a + b, fun i ↦ by simpa using add_mem (ha i) (hb i), by simp [ha', hb']⟩
    | smul a b hb hb' =>
      obtain ⟨b', hb, hb'⟩ := hb'
      have ⟨p, hp⟩ := adjoin_eq_exists_aeval R x a
      refine ⟨p * b', fun i ↦ ?_, by simp [hp, hb']⟩
      rw [coeff_mul]
      exact sum_mem fun i hi ↦ Ideal.mul_mem_left _ _ (hb _)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
H : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
mp :
  ∀ (a : ↥R[x]) (ha : Membership.mem (γ := Set ↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R)) a),
    ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
have mp₁ : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) ((↑0 : S) : S)
Tactic: induction H using Submodule.span_induction with
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      exact ⟨C a, fun i ↦ by rw [coeff_C]; aesop, aeval_C _ _⟩
    | zero => exact ⟨0, by simp, aeval_zero _⟩
    | add a b ha hb ha' hb' =>
      obtain ⟨a, ha, ha'⟩ := ha'
      obtain ⟨b, hb, hb'⟩ := hb'
      exact ⟨a + b, fun i ↦ by simpa using add_mem (ha i) (hb i), by simp [ha', hb']⟩
    | smul a b hb hb' =>
      obtain ⟨b', hb, hb'⟩ := hb'
      have ⟨p, hp⟩ := adjoin_eq_exists_aeval R x a
      refine ⟨p * b', fun i ↦ ?_, by simp [hp, hb']⟩
      rw [coeff_mul]
      exact sum_mem fun i hi ↦ Ideal.mul_mem_left _ _ (hb _)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
H : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
mp :
  ∀ (a : ↥R[x]) (ha : Membership.mem (γ := Set ↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R)) a),
    ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S)
mp₁ : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) ((↑0 : S) : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : S)
have mp₂ : ∀ (a b : ↥R[x])
  (ha :
    Membership.mem (γ := Submodule ↥R[x] ↥R[x])
      (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) a)
  (hb :
    Membership.mem (γ := Submodule ↥R[x] ↥R[x])
      (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b)
  (ha' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S))
  (hb' : ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑b : S)),
  ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a + b) : S)
Tactic: induction H using Submodule.span_induction with
    | mem a ha =>
      obtain ⟨a, ha, rfl⟩ := ha
      exact ⟨C a, fun i ↦ by rw [coeff_C]; aesop, aeval_C _ _⟩
    | zero => exact ⟨0, by simp, aeval_zero _⟩
    | add a b ha hb ha' hb' =>
      obtain ⟨a, ha, ha'⟩ := ha'
      obtain ⟨b, hb, hb'⟩ := hb'
      exact ⟨a + b, fun i ↦ by simpa using add_mem (ha i) (hb i), by simp [ha', hb']⟩
    | smul a b hb hb' =>
      obtain ⟨b', hb, hb'⟩ := hb'
      have ⟨p, hp⟩ := adjoin_eq_exists_aeval R x a
      refine ⟨p * b', fun i ↦ ?_, by simp [hp, hb']⟩
      rw [coeff_mul]
      exact sum_mem fun i hi ↦ Ideal.mul_mem_left _ _ (hb _)
Cleared hypotheses: H