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)
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
rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]
no goals
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)
exact B (support p)
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)
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)
intro n a
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)

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)
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)
induction' n with n ih
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)
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)
rw [pow_zero, mul_one]
no goals
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)
exact h_C a
no goals
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)
exact h_monomial _ _ ih
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)

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)
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)
apply Finset.induction
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
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)
convert h_C 0
no goals
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
exact C_0.symm
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)
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)
intro n s ns ih
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)
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)
rw [sum_insert ns]
no goals
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)
exact h_add _ _ A ih