-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem mem_span_C_coeff : f ∈ Ideal.span { g : R[X] | ∃ i : ℕ, g = C (coeff f i) }

Proof state:
case a
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ C (f.coeff n) ∈ {g | ∃ i, g = C (f.coeff i)}

Tactic:
rw [mem_setOf_eq]

Result:
case a
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ ∃ i, C (f.coeff n) = C (f.coeff i)

Proof state:
case a
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ ∃ i, C (f.coeff n) = C (f.coeff i)

Tactic:
use n

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this : C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this

Result:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Proof state:
case h.e'_5
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n = (monomial n) (f.coeff n)

Tactic:
rw [← C_mul_X_pow_eq_monomial]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
⊢ (f.sum fun n a => C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
refine Submodule.sum_mem _ fun n _hn => ?_

Result:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ (fun n a => C a * X ^ n) n (f.coeff n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
have : C (coeff f n) ∈ p := by
  apply subset_span
  rw [mem_setOf_eq]
  use n

Result:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this : C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ C (f.coeff n) ∈ p

Tactic:
apply subset_span

Result:
case a
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ C (f.coeff n) ∈ {g | ∃ i, g = C (f.coeff i)}

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
convert this using 1

Result:
case h.e'_5
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n = (monomial n) 1 • C (f.coeff n)

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
⊢ f ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
nth_rw 2 [(sum_C_mul_X_pow_eq f).symm]

Result:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
⊢ (f.sum fun n a => C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ (fun n a => C a * X ^ n) n (f.coeff n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
dsimp

Result:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
let p := Ideal.span { g : R[X] | ∃ i : ℕ, g = C (coeff f i) }

Result:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
⊢ f ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Proof state:
case h.e'_5
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n = (monomial n) 1 • C (f.coeff n)

Tactic:
simp only [monomial_mul_C, one_mul, smul_eq_mul]

Result:
case h.e'_5
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n = (monomial n) (f.coeff n)