awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
rw₄ 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
⊢ 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

Tactic:
rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]

Premises used: eq_add_of_sub_eq', Polynomial.C_mul, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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
⊢ ∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
    HMul.hMul (β := R[X][X]) a_1
          ((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]) +
        b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
      P

Tactic:
exact ⟨C p, q, by rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]⟩
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
x : R
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
⊢ 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])})

Tactic:
ext y
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
x : R
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:
simp [Ideal.mem_span_singleton, dvd_iff_isRoot, RingHom.mem_ker]

Premises used: RingHom.mem_ker, Polynomial.dvd_iff_isRoot, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
q : R[X]
hq : q.Monic
⊢ q.modByMonicHom.ker = Submodule.restrictScalars R (Ideal.span {q})

Tactic:
Submodule.ext fun _ => (mem_ker_modByMonic hq).trans Ideal.mem_span_singleton.symm

Premises used: Polynomial.mem_ker_modByMonic, Iff.trans, Ideal.mem_span_singleton, Iff.symm, Submodule.ext
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
⊢ LE.le (α := Ideal R[X]) (Ideal.span {X}) (RingHom.ker (F := R[X] →+* R) constantCoeff)

Tactic:
simp [Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
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
⊢ Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →+* R) constantCoeff) (Ideal.span {X})

Tactic:
refine le_antisymm (fun p hp ↦ ?_) (by simp [Ideal.span_le])

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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
⊢ X ∣ p

Tactic:
simp only [RingHom.mem_ker, constantCoeff_apply, ← Polynomial.X_dvd_iff] at hp

Premises used: Polynomial.constantCoeff_apply, RingHom.mem_ker, Polynomial.X_dvd_iff
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
hp : X ∣ p
rwa rwa₁ rwa₂ rwa₃ : X ∣ p
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span {X}) p

Tactic:
rwa [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
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
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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
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)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑a : S)

Tactic:
obtain ⟨a, ha, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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 : ℕ
rw : (if i = 0 then a else 0) ∈ I
⊢ coeff ((C : (a : R) → R[X]) a) i ∈ I

Tactic:
rw [coeff_C]

Premises used: Polynomial.coeff_C
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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 : ℕ
⊢ (if i = 0 then a else 0) ∈ I

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
⊢ ∃ (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:
exact ⟨C a, fun i ↦ by rw [coeff_C]; aesop, aeval_C _ _⟩
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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]
⊢ ∀ (i : ℕ), coeff 0 i ∈ I

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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]
⊢ ∃ (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:
exact ⟨0, by simp, aeval_zero _⟩
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
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)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a + b) : S)

Tactic:
obtain ⟨a, ha, ha'⟩ := ha'
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
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)
⊢ ∃ (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'
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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_1 : ↥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_1 :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b_1
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x : (a : R[X]) → S) a = (↑a_1 : S)
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x : (a : R[X]) → S) b = (↑b_1 : S)
i : ℕ
⊢ (a + b).coeff i ∈ I

Tactic:
simpa using add_mem (ha i) (hb i)

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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_1 : ↥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_1 :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b_1
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x : (a : R[X]) → S) a = (↑a_1 : S)
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x : (a : R[X]) → S) b = (↑b_1 : S)
⊢ (aeval x : (a : R[X]) → S) (a + b) = (↑(a_1 + b_1) : S)

Tactic:
simp [ha', hb']
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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_1 : ↥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_1 :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (Submodule.span (↥R[x]) ((⇑(algebraMap R ↥R[x]) : (a : R) → ↥R[x]) '' (↑I : Set R))) b_1
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x : (a : R[X]) → S) a = (↑a_1 : S)
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x : (a : R[X]) → S) b = (↑b_1 : S)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a_1 + b_1) : S)

Tactic:
exact ⟨a + b, fun i ↦ by simpa using add_mem (ha i) (hb i), by simp [ha', hb']⟩
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
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)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a • b) : S)

Tactic:
obtain ⟨b', hb, hb'⟩ := hb'
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
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)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
⊢ (aeval x : (a : R[X]) → S) (p * b') = (↑(a • b) : S)

Tactic:
simp [hp, hb']
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
mp : ∀ (i : ℕ), (p * b').coeff i ∈ I
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑(a • b) : S)

Tactic:
refine ⟨p * b', fun i ↦ ?_, by simp [hp, hb']⟩
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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 : ℕ
mp : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ i, p.coeff x.1 * b'.coeff x.2 ∈ I
⊢ (p * b').coeff i ∈ I

Tactic:
rw [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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 : ℕ
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ i, p.coeff x.1 * b'.coeff x.2 ∈ I

Tactic:
sum_mem fun i hi ↦ Ideal.mul_mem_left _ _ (hb _)

Premises used: Prod.fst, Polynomial.coeff, Ideal.mul_mem_left, Prod.snd, sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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 : ℕ
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ i, p.coeff x.1 * b'.coeff x.2 ∈ I

Tactic:
exact sum_mem fun i hi ↦ Ideal.mul_mem_left _ _ (hb _)

Premises used: Ideal.mul_mem_left, sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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)
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)
mp₃ :
  ∀ (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)
⊢ ∃ (p : R[X]), (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x : (a : R[X]) → S) p = (↑y : 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 _)

Premises used: Polynomial.coeff_mul, rfl
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
trans :
  y =
    ∑ i ∈ p.support,
      Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        ((aeval x : (a : R[X]) → S)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)))
        ⋯
trans₁ :
  Eq.{u_2 + 1} (α := ↥R[x])
    (∑ i ∈ p.support,
      Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        ((aeval x : (a : R[X]) → S)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)))
        ⋯)
    (∑ i ∈ p.support,
      HSMul.hSMul (β := ↥R[x]) (p.coeff i)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
          ↥R[x]))
⊢ y =
    ∑ i ∈ p.support,
      HSMul.hSMul (β := ↥R[x]) (p.coeff i)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S) (HPow.hPow (α := R[X]) X i)) ⋯ :
          ↥R[x])

Tactic:
trans ∑ i ∈ p.support, ⟨_, (C (p.coeff i) * X ^ i).aeval_mem_adjoin_singleton _ x⟩

Premises used: Polynomial.support
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
a :
  (↑y : S) =
    (↑(∑ i ∈ p.support,
          Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S)
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)))
            ⋯) :
      S)
⊢ y =
    ∑ i ∈ p.support,
      Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        ((aeval x : (a : R[X]) → S)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)))
        ⋯

Tactic:
ext1
-- Module: Mathlib.RingTheory.Polynomial.Ideal
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]
p : R[X]
hp : ∀ (i : ℕ), p.coeff i ∈ I
hp' : (aeval x : (a : R[X]) → S) p = (↑y : S)
⊢ (↑y : S) =
    (↑(∑ i ∈ p.support,
          Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            ((aeval x : (a : R[X]) → S)
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)))
            ⋯) :
      S)

Tactic:
simp only [AddSubmonoidClass.coe_finsetSum, ← map_sum, ← hp', ← as_sum_support_C_mul_X_pow]

Premises used: Polynomial.as_sum_support_C_mul_X_pow, AddSubmonoidClass.coe_finsetSum, map_sum