-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem coeff_comp_degree_mul_degree (hqd0 : natDegree q ≠ 0) :
    coeff (p.comp q) (natDegree p * natDegree q) =
    leadingCoeff p * leadingCoeff q ^ natDegree p

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (C (p.coeff b)).natDegree + (q ^ b).natDegree < p.natDegree * q.natDegree

Tactic:
rw [natDegree_C, zero_add]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (q ^ b).natDegree < p.natDegree * q.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]

Result:
no goals

Proof state:
case h₀
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

case h₂
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
case h₂ =>
  simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]

Result:
case h₀
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
rw [comp, eval₂_def, coeff_sum]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.sum fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

Tactic:
simp +contextual

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.sum fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂

Result:
case h₀
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

case h₂
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Proof state:
case h₀
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

Tactic:
case h₀ =>
  intro b hbs hbp
  refine coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt ?_)
  rw [natDegree_C, zero_add]
  refine natDegree_pow_le.trans_lt ((mul_lt_mul_right (pos_iff_ne_zero.mpr hqd0)).mpr ?_)
  exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp

Result:
case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (q ^ b).natDegree < p.natDegree * q.natDegree

Tactic:
refine natDegree_pow_le.trans_lt ((mul_lt_mul_right (pos_iff_ne_zero.mpr hqd0)).mpr ?_)

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ b < p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

Tactic:
intro b hbs hbp

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ b < p.natDegree

Tactic:
exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp

Result:
no goals

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

Tactic:
case h₁ =>
  simp +contextual

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

Tactic:
refine coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt ?_)

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (C (p.coeff b)).natDegree + (q ^ b).natDegree < p.natDegree * q.natDegree