-- Mathlib/Algebra/Polynomial/Basic.lean
theorem induction_on {M : R[X] → Prop} (p : R[X]) (h_C : ∀ a, M (C a))
    (h_add : ∀ p q, 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

Proof state:
case empty
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ ∅, C (p.coeff n) * X ^ n)

Tactic:
convert h_C 0

Result:
case h.e'_1
R : Type u
inst✝ : Semiring R
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 ∈ ∅, C (p.coeff n) * X ^ n = C 0

Proof state:
R : Type u
inst✝ : Semiring R
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)

Tactic:
intro n a

Result:
R : Type u
inst✝ : Semiring R
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)

Proof state:
case zero
R : Type u
inst✝ : Semiring R
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 ^ 0)

Tactic:
rw [pow_zero, mul_one]

Result:
case zero
R : Type u
inst✝ : Semiring R
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)

Proof state:
case insert
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n)
⊢ M (∑ n ∈ insert n s, C (p.coeff n) * X ^ n)

Tactic:
rw [sum_insert ns]

Result:
case insert
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n)
⊢ M (C (p.coeff n) * X ^ n + ∑ x ∈ s, C (p.coeff x) * X ^ x)

Proof state:
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n)
⊢ M p

Tactic:
rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]

Result:
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n)
⊢ M (∑ n ∈ p.support, C (p.coeff n) * X ^ n)

Proof state:
case succ
R : Type u
inst✝ : Semiring R
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 ^ (n + 1))

Tactic:
exact h_monomial _ _ ih

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
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)

Tactic:
exact h_C a

Result:
no goals

Proof state:
case insert
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n)
⊢ M (C (p.coeff n) * X ^ n + ∑ x ∈ s, C (p.coeff x) * X ^ x)

Tactic:
exact h_add _ _ A ih

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
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)

Tactic:
induction n with
| zero => rw [pow_zero, mul_one]; exact h_C a
| succ n ih => exact h_monomial _ _ ih

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n)

Tactic:
apply Finset.induction

Result:
case empty
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ ∅, C (p.coeff n) * X ^ n)

case insert
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n) → M (∑ n ∈ insert a s, C (p.coeff n) * X ^ n)

Proof state:
R : Type u
inst✝ : Semiring R
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

Tactic:
have A : ∀ {n : ℕ} {a}, M (C a * X ^ n) := by
  intro n a
  induction n with
  | zero => rw [pow_zero, mul_one]; exact h_C a
  | succ n ih => exact h_monomial _ _ ih

Result:
R : Type u
inst✝ : Semiring R
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

Proof state:
case insert
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n) → M (∑ n ∈ insert a s, C (p.coeff n) * X ^ n)

Tactic:
intro n s ns ih

Result:
case insert
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n)
⊢ M (∑ n ∈ insert n s, C (p.coeff n) * X ^ n)

Proof state:
case h.e'_1
R : Type u
inst✝ : Semiring R
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 ∈ ∅, C (p.coeff n) * X ^ n = C 0

Tactic:
exact C_0.symm

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
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 (∑ n ∈ s, C (p.coeff n) * X ^ n)
⊢ M (∑ n ∈ p.support, C (p.coeff n) * X ^ n)

Tactic:
exact B (support p)

Result:
no goals