R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (sum p fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) = leadingCoeff p * leadingCoeff q ^ natDegree p
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ coeff (comp p q) (natDegree p * natDegree q) = leadingCoeff p * leadingCoeff q ^ natDegree p
rw [comp, eval₂_def, coeff_sum]
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0

case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0

case h₂
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) =
    leadingCoeff p * leadingCoeff q ^ natDegree p
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (sum p fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) = leadingCoeff p * leadingCoeff q ^ natDegree p
refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0

case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0

case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0

case h₂
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) =
    leadingCoeff p * leadingCoeff q ^ natDegree p
case h₂ =>
  simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0

case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
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
no goals
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
case h₁ =>
  simp (config := { contextual := true })
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) =
    leadingCoeff p * leadingCoeff q ^ natDegree p
simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0
intro b hbs hbp
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ natDegree (↑C (coeff p b)) + natDegree (q ^ b) < natDegree p * natDegree q
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0
refine' coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt _)
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ natDegree (q ^ b) < natDegree p * natDegree q
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ natDegree (↑C (coeff p b)) + natDegree (q ^ b) < natDegree p * natDegree q
rw [natDegree_C, zero_add]
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ b < natDegree p
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ natDegree (q ^ b) < natDegree p * natDegree q
refine' natDegree_pow_le.trans_lt ((mul_lt_mul_right (pos_iff_ne_zero.mpr hqd0)).mpr _)
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ b < natDegree p
exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
simp (config := { contextual := true })