R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
⊢ f ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
I : Ideal R[X]
⊢ f ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
let p := Ideal.span { g : R[X] | ∃ i : ℕ, g = C (coeff f i) }
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
⊢ (sum f fun n a => ↑C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
⊢ f ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
nth_rw 1 [(sum_C_mul_X_pow_eq f).symm]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ (fun n a => ↑C a * X ^ n) n (coeff f n) ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
⊢ (sum f fun n a => ↑C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
refine' Submodule.sum_mem _ fun n _hn => _
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ (fun n a => ↑C a * X ^ n) n (coeff f n) ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
dsimp
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this : ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
have : C (coeff f n) ∈ p := by
  apply subset_span
  rw [mem_setOf_eq]
  use n
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this : ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this
case h.e'_4
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n = ↑(monomial n) 1 • ↑C (coeff f n)
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
convert this using 1
case h.e'_4
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n = ↑(monomial n) (coeff f n)
case h.e'_4
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n = ↑(monomial n) 1 • ↑C (coeff f n)
simp only [monomial_mul_C, one_mul, smul_eq_mul]
no goals
case h.e'_4
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n = ↑(monomial n) (coeff f n)
rw [← C_mul_X_pow_eq_monomial]
case a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ↑C (coeff f n) ∈ {g | ∃ i, g = ↑C (coeff f i)}
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ↑C (coeff f n) ∈ p
apply subset_span
case a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ∃ i, ↑C (coeff f n) = ↑C (coeff f i)
case a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ↑C (coeff f n) ∈ {g | ∃ i, g = ↑C (coeff f i)}
rw [mem_setOf_eq]
no goals
case a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ∃ i, ↑C (coeff f n) = ↑C (coeff f i)
use n