[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
⊢ M p
[PROOFSTEP]
have A : ∀ {n : ℕ} {a}, M (C a * X ^ n) := by
  intro n a
  induction' n with n ih
  · rw [pow_zero, mul_one]; exact h_C a
  · exact h_monomial _ _ ih
[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
⊢ ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
[PROOFSTEP]
intro n a
[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
n : ℕ
a : R
⊢ M (↑C a * X ^ n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
a : R
⊢ M (↑C a * X ^ Nat.zero)
[PROOFSTEP]
rw [pow_zero, mul_one]
[GOAL]
case zero
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
a : R
⊢ M (↑C a)
[PROOFSTEP]
exact h_C a
[GOAL]
case succ
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
a : R
n : ℕ
ih : M (↑C a * X ^ n)
⊢ M (↑C a * X ^ Nat.succ n)
[PROOFSTEP]
exact h_monomial _ _ ih
[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ M p
[PROOFSTEP]
have B : ∀ s : Finset ℕ, M (s.sum fun n : ℕ => C (p.coeff n) * X ^ n) :=
  by
  apply Finset.induction
  · convert h_C 0
    exact C_0.symm
  · intro n s ns ih
    rw [sum_insert ns]
    exact h_add _ _ A ih
[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ ∀ (s : Finset ℕ), M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
apply Finset.induction
[GOAL]
case empty
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ M (Finset.sum ∅ fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
convert h_C 0
[GOAL]
case h.e'_1
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ (Finset.sum ∅ fun n => ↑C (coeff p n) * X ^ n) = ↑C 0
[PROOFSTEP]
exact C_0.symm
[GOAL]
case insert
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ},
    ¬a ∈ s →
      M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n) → M (Finset.sum (insert a s) fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
intro n s ns ih
[GOAL]
case insert
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
n : ℕ
s : Finset ℕ
ns : ¬n ∈ s
ih : M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
⊢ M (Finset.sum (insert n s) fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
rw [sum_insert ns]
[GOAL]
case insert
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
n : ℕ
s : Finset ℕ
ns : ¬n ∈ s
ih : M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
⊢ M (↑C (coeff p n) * X ^ n + Finset.sum s fun x => ↑C (coeff p x) * X ^ x)
[PROOFSTEP]
exact h_add _ _ A ih
[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
B : ∀ (s : Finset ℕ), M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
⊢ M p
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]
[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
B : ∀ (s : Finset ℕ), M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
⊢ M (Finset.sum (support p) fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
exact B (support p)
[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑(monomial n) a)
n : ℕ
a : R
_h : M (↑C a * X ^ n)
⊢ M (↑C a * X ^ (n + 1))
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial]
[GOAL]
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 : R[X]
M : R[X] → Prop
p : R[X]
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑(monomial n) a)
n : ℕ
a : R
_h : M (↑C a * X ^ n)
⊢ M (↑(monomial (n + 1)) a)
[PROOFSTEP]
exact h_monomial _ _
[GOAL]
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]
cf : ∀ (i : ℕ), ↑C (coeff f i) ∈ I
⊢ Ideal.span {g | ∃ i, g = ↑C (coeff f i)} ≤ I
[PROOFSTEP]
simp (config := { singlePass := true }) only [@eq_comm _ _ (C _)]
[GOAL]
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]
cf : ∀ (i : ℕ), ↑C (coeff f i) ∈ I
⊢ Ideal.span {g | ∃ i, ↑C (coeff f i) = g} ≤ I
[PROOFSTEP]
exact (Ideal.span_le.trans range_subset_iff).mpr cf
[GOAL]
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)}
[PROOFSTEP]
let p := Ideal.span {g : R[X] | ∃ i : ℕ, g = C (coeff f i)}
[GOAL]
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)}
[PROOFSTEP]
nth_rw 1 [(sum_C_mul_X_pow_eq f).symm]
[GOAL]
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)}
[PROOFSTEP]
refine' Submodule.sum_mem _ fun n _hn => _
[GOAL]
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)}
[PROOFSTEP]
dsimp
[GOAL]
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)}
[PROOFSTEP]
have : C (coeff f n) ∈ p := by
  apply subset_span
  rw [mem_setOf_eq]
  use n
[GOAL]
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
[PROOFSTEP]
apply subset_span
[GOAL]
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)}
[PROOFSTEP]
rw [mem_setOf_eq]
[GOAL]
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)
[PROOFSTEP]
use n
[GOAL]
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)}
[PROOFSTEP]
have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this
[GOAL]
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)}
[PROOFSTEP]
convert this using 1
[GOAL]
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)
[PROOFSTEP]
simp only [monomial_mul_C, one_mul, smul_eq_mul]
[GOAL]
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)
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial]
