[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : DecidableEq R
⊢ Decidable (Monic p)
[PROOFSTEP]
unfold Monic
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : DecidableEq R
⊢ Decidable (leadingCoeff p = 1)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Subsingleton R
⊢ degree p = ⊥
[PROOFSTEP]
rw [Subsingleton.elim p 0, degree_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Subsingleton R
⊢ natDegree p = 0
[PROOFSTEP]
rw [Subsingleton.elim p 0, natDegree_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
⊢ degree p = ↑(natDegree p)
[PROOFSTEP]
let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt degree_eq_bot.1 hp))
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬¬n ∈ degree p
⊢ degree p = ↑(natDegree p)
[PROOFSTEP]
have hn : degree p = some n := Classical.not_not.1 hn
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ degree p
hn : degree p = Option.some n
⊢ degree p = ↑(natDegree p)
[PROOFSTEP]
rw [natDegree, hn]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ degree p
hn : degree p = Option.some n
⊢ Option.some n = ↑(WithBot.unbot' 0 (Option.some n))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ degree p = ↑n ↔ natDegree p = n
[PROOFSTEP]
rw [degree_eq_natDegree hp]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑(natDegree p) = ↑n ↔ natDegree p = n
[PROOFSTEP]
exact WithBot.coe_eq_coe
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ degree p = ↑n ↔ natDegree p = n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ degree p = ↑n → natDegree p = n
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : degree p = ↑n
⊢ natDegree p = n
[PROOFSTEP]
rwa [← degree_eq_iff_natDegree_eq]
[GOAL]
case mp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : degree p = ↑n
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : degree 0 = ↑n
⊢ False
[PROOFSTEP]
rw [degree_zero] at H
[GOAL]
case mp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : ⊥ = ↑n
⊢ False
[PROOFSTEP]
exact Option.noConfusion H
[GOAL]
case mpr
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ natDegree p = n → degree p = ↑n
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natDegree p = n
⊢ degree p = ↑n
[PROOFSTEP]
rwa [degree_eq_iff_natDegree_eq]
[GOAL]
case mpr
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natDegree p = n
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : natDegree 0 = n
⊢ False
[PROOFSTEP]
rw [natDegree_zero] at H
[GOAL]
case mpr
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : 0 = n
⊢ False
[PROOFSTEP]
rw [H] at hn
[GOAL]
case mpr
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n < n
H : 0 = n
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hn
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : degree p = ↑n
⊢ natDegree p = n
[PROOFSTEP]
rw [natDegree, h, Nat.cast_withBot, WithBot.unbot'_coe]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : degree p = degree q
⊢ natDegree p = natDegree q
[PROOFSTEP]
unfold natDegree
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : degree p = degree q
⊢ WithBot.unbot' 0 (degree p) = WithBot.unbot' 0 (degree q)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ n ≤ natDegree p
[PROOFSTEP]
rw [← Nat.cast_le (α := WithBot ℕ), ← degree_eq_natDegree]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ ↑n ≤ degree p
R : Type u S : Type v a b c d : R n m : ℕ inst✝ : Semiring R p q r : R[X] h : coeff p n ≠ 0 ⊢ p ≠ 0
[PROOFSTEP]
exact le_degree_of_ne_zero h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
q r : R[X]
h : coeff 0 n ≠ 0
⊢ False
[PROOFSTEP]
exact h rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
⊢ degree p ≤ degree q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
hp : p = 0
⊢ degree p ≤ degree q
[PROOFSTEP]
rw [hp]
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
hp : p = 0
⊢ degree 0 ≤ degree q
[PROOFSTEP]
exact bot_le
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
hp : ¬p = 0
⊢ degree p ≤ degree q
[PROOFSTEP]
rw [degree_eq_natDegree hp]
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
hp : ¬p = 0
⊢ ↑(natDegree p) ≤ degree q
[PROOFSTEP]
exact le_degree_of_ne_zero h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : p ≠ 0
hpq : degree p < degree q
⊢ natDegree p < natDegree q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : p ≠ 0
hpq : degree p < degree q
hq : q = 0
⊢ natDegree p < natDegree q
[PROOFSTEP]
exact (not_lt_bot <| hq ▸ hpq).elim
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : p ≠ 0
hpq : degree p < degree q
hq : ¬q = 0
⊢ natDegree p < natDegree q
[PROOFSTEP]
rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ degree (↑C a) = 0
[PROOFSTEP]
rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton, WithBot.coe_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ degree (↑C a) ≤ 0
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a = 0
⊢ degree (↑C a) ≤ 0
[PROOFSTEP]
rw [h, C_0]
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a = 0
⊢ degree 0 ≤ 0
[PROOFSTEP]
exact bot_le
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : ¬a = 0
⊢ degree (↑C a) ≤ 0
[PROOFSTEP]
rw [degree_C h]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ degree 1 ≤ 0
[PROOFSTEP]
rw [← C_1]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ degree (↑C 1) ≤ 0
[PROOFSTEP]
exact degree_C_le
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
⊢ natDegree (↑C a) = 0
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
⊢ natDegree (↑C a) = 0
[PROOFSTEP]
have : C a = 0 := by rw [ha, C_0]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
⊢ ↑C a = 0
[PROOFSTEP]
rw [ha, C_0]
[GOAL]
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
this : ↑C a = 0
⊢ natDegree (↑C a) = 0
[PROOFSTEP]
rw [natDegree, degree_eq_bot.2 this]
[GOAL]
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
this : ↑C a = 0
⊢ WithBot.unbot' 0 ⊥ = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : ¬a = 0
⊢ natDegree (↑C a) = 0
[PROOFSTEP]
rw [natDegree, degree_C ha]
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : ¬a = 0
⊢ WithBot.unbot' 0 0 = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ natDegree ↑n = 0
[PROOFSTEP]
simp only [← C_eq_nat_cast, natDegree_C]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ natDegree ↑n ≤ Zero.zero
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
ha : a ≠ 0
⊢ degree (↑(monomial n) a) = ↑n
[PROOFSTEP]
rw [degree, support_monomial n ha]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
ha : a ≠ 0
⊢ Finset.max {n} = ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
ha : a ≠ 0
⊢ degree (↑C a * X ^ n) = ↑n
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ degree (↑C a * X) = 1
[PROOFSTEP]
simpa only [pow_one] using degree_C_mul_X_pow 1 ha
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
h : a = 0
⊢ degree (↑(monomial n) a) ≤ ↑n
[PROOFSTEP]
rw [h, (monomial n).map_zero]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
h : a = 0
⊢ degree 0 ≤ ↑n
[PROOFSTEP]
exact bot_le
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ degree (↑C a * X ^ n) ≤ ↑n
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ degree (↑(monomial n) a) ≤ ↑n
[PROOFSTEP]
apply degree_monomial_le
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
⊢ degree (↑C a * X) ≤ 1
[PROOFSTEP]
simpa only [pow_one] using degree_C_mul_X_pow_le 1 a
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a ≠ 0
⊢ natDegree (↑C a * X) = 1
[PROOFSTEP]
simpa only [pow_one] using natDegree_C_mul_X_pow 1 a ha
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : DecidableEq R
i : ℕ
r : R
⊢ natDegree (↑(monomial i) r) = if r = 0 then 0 else i
[PROOFSTEP]
split_ifs with hr
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ natDegree (↑(monomial i) r) = 0
[PROOFSTEP]
simp [hr]
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ natDegree (↑(monomial i) r) = i
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
⊢ natDegree (↑(monomial m) a) ≤ m
[PROOFSTEP]
rw [Polynomial.natDegree_monomial]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
⊢ (if a = 0 then 0 else m) ≤ m
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
h✝ : a = 0
⊢ 0 ≤ m
case neg R : Type u S : Type v a✝ b c d : R n m✝ : ℕ inst✝ : Semiring R p q r : R[X] a : R m : ℕ h✝ : ¬a = 0 ⊢ m ≤ m
[PROOFSTEP]
exacts [Nat.zero_le _, rfl.le]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
⊢ coeff p n = 0
[PROOFSTEP]
apply coeff_eq_zero_of_degree_lt
[GOAL]
case h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
⊢ degree p < ↑n
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
hp : p = 0
⊢ degree p < ↑n
[PROOFSTEP]
subst hp
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
h : natDegree 0 < n
⊢ degree 0 < ↑n
[PROOFSTEP]
exact WithBot.bot_lt_coe n
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
hp : ¬p = 0
⊢ degree p < ↑n
[PROOFSTEP]
rwa [degree_eq_natDegree hp, Nat.cast_lt]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
⊢ p = q ↔ ∀ (i : ℕ), i ≤ n → coeff p i = coeff q i
[PROOFSTEP]
refine' Iff.trans Polynomial.ext_iff _
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
⊢ (∀ (n : ℕ), coeff p n = coeff q n) ↔ ∀ (i : ℕ), i ≤ n → coeff p i = coeff q i
[PROOFSTEP]
refine' forall_congr' fun i => ⟨fun h _ => h, fun h => _⟩
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
i : ℕ
h : i ≤ n → coeff p i = coeff q i
⊢ coeff p i = coeff q i
[PROOFSTEP]
refine' (le_or_lt i n).elim h fun k => _
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
hp : natDegree p ≤ n
hq : natDegree q ≤ n
i : ℕ
h : i ≤ n → coeff p i = coeff q i
k : n < i
⊢ coeff p i = coeff q i
[PROOFSTEP]
exact (coeff_eq_zero_of_natDegree_lt (hp.trans_lt k)).trans (coeff_eq_zero_of_natDegree_lt (hq.trans_lt k)).symm
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
I : Decidable (n < 1 + natDegree p)
⊢ (if n < 1 + natDegree p then coeff p n else 0) = coeff p n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
I : Decidable (n < 1 + natDegree p)
h : n < 1 + natDegree p
⊢ coeff p n = coeff p n
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
I : Decidable (n < 1 + natDegree p)
h : ¬n < 1 + natDegree p
⊢ 0 = coeff p n
[PROOFSTEP]
exact (coeff_eq_zero_of_natDegree_lt (not_le.1 fun w => h (Nat.lt_one_add_iff.2 w))).symm
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ ∑ i in support p, ↑(monomial i) (coeff p i) = ∑ i in support p, ↑C (coeff p i) * X ^ i
[PROOFSTEP]
simp only [C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
w : natDegree p < n
⊢ sum p f = ∑ a in range n, f a (coeff p a)
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
⊢ sum { toFinsupp := toFinsupp✝ } f = ∑ a in range n, f a (coeff { toFinsupp := toFinsupp✝ } a)
[PROOFSTEP]
have := supp_subset_range w
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
this : support { toFinsupp := toFinsupp✝ } ⊆ range n
⊢ sum { toFinsupp := toFinsupp✝ } f = ∑ a in range n, f a (coeff { toFinsupp := toFinsupp✝ } a)
[PROOFSTEP]
simp only [Polynomial.sum, support, coeff, natDegree, degree] at this ⊢
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
this : toFinsupp✝.support ⊆ range n
⊢ ∑ x in toFinsupp✝.support, f x (↑toFinsupp✝ x) = ∑ x in range n, f x (↑toFinsupp✝ x)
[PROOFSTEP]
exact Finsupp.sum_of_support_subset _ this _ fun n _hn => h n
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
⊢ ∑ i : Fin n, f (↑i) (coeff p ↑i) = sum p f
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
⊢ ∑ i : Fin n, f (↑i) (coeff p ↑i) = sum p f
[PROOFSTEP]
rw [hp, sum_zero_index, Finset.sum_eq_zero]
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
⊢ ∀ (x : Fin n), x ∈ univ → f (↑x) (coeff 0 ↑x) = 0
[PROOFSTEP]
intro i _
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
i : Fin n
a✝ : i ∈ univ
⊢ f (↑i) (coeff 0 ↑i) = 0
[PROOFSTEP]
exact hf i
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : ¬p = 0
⊢ ∑ i : Fin n, f (↑i) (coeff p ↑i) = sum p f
[PROOFSTEP]
rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn), Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ ∑ i in range (natDegree p + 1), ↑(monomial i) (coeff p i) = ∑ i in range (natDegree p + 1), ↑C (coeff p i) * X ^ i
[PROOFSTEP]
simp only [C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n : ℕ
⊢ coeff p Nat.zero = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝¹ m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n✝ n : ℕ
⊢ coeff p (Nat.succ Nat.zero) = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) (Nat.succ Nat.zero)
[PROOFSTEP]
simp [coeff_C]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝¹ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n✝ n m : ℕ
⊢ coeff p (Nat.succ (Nat.succ m)) = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) (Nat.succ (Nat.succ m))
[PROOFSTEP]
have : degree p < m.succ.succ := lt_of_le_of_lt h (Iff.mpr WithBot.coe_lt_coe <| Nat.succ_lt_succ <| Nat.zero_lt_succ m)
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝¹ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n✝ n m : ℕ
this : degree p < ↑(Nat.succ (Nat.succ m))
⊢ coeff p (Nat.succ (Nat.succ m)) = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) (Nat.succ (Nat.succ m))
[PROOFSTEP]
simp [coeff_eq_zero_of_degree_lt this, coeff_C, Nat.succ_ne_zero, coeff_X, Nat.succ_inj', @eq_comm ℕ 0]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p = 1
⊢ ↑C (coeff p 1) * X + ↑C (coeff p 0) = ↑C (leadingCoeff p) * X + ↑C (coeff p 0)
[PROOFSTEP]
simp only [leadingCoeff, natDegree_eq_of_degree_eq_some h]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p = 1
⊢ ↑C (coeff p 1) * X + ↑C (coeff p 0) = ↑C (coeff p One.one) * X + ↑C (coeff p 0)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hm : Monic p
hnd : natDegree p = 1
⊢ p = X + ↑C (coeff p 0)
[PROOFSTEP]
rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ degree (X ^ n) ≤ ↑n
[PROOFSTEP]
simpa only [C_1, one_mul] using degree_C_mul_X_pow_le n (1 : R)
[GOAL]
R : Type u
S : Type v
a b c✝ d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
c : R
n : ℕ
⊢ card (support (↑C c * X ^ n)) ≤ 1
[PROOFSTEP]
rw [← card_singleton n]
[GOAL]
R : Type u
S : Type v
a b c✝ d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
c : R
n : ℕ
⊢ card (support (↑C c * X ^ n)) ≤ card {n}
[PROOFSTEP]
apply card_le_of_subset (support_C_mul_X_pow' n c)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ card (support p) ≤ natDegree p + 1
[PROOFSTEP]
rw [← Finset.card_range (p.natDegree + 1)]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ card (support p) ≤ card (range (natDegree p + 1))
[PROOFSTEP]
exact Finset.card_le_of_subset supp_subset_range_natDegree_succ
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ Finset.Nonempty (support p) ↔ p ≠ 0
[PROOFSTEP]
rw [Ne.def, nonempty_iff_ne_empty, Ne.def, ← support_eq_empty]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Ring R
p : R[X]
r : R
a : ℕ
⊢ coeff (p * (X - ↑C r)) (a + 1) = coeff p a - coeff p (a + 1) * r
[PROOFSTEP]
simp [mul_sub]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ degree (-p) = degree p
[PROOFSTEP]
unfold degree
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ Finset.max (support (-p)) = Finset.max (support p)
[PROOFSTEP]
rw [support_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ natDegree (-p) = natDegree p
[PROOFSTEP]
simp [natDegree]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Ring R
n : ℤ
⊢ natDegree ↑n = 0
[PROOFSTEP]
rw [← C_eq_int_cast, natDegree_C]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Ring R
n : ℤ
⊢ natDegree ↑n ≤ Zero.zero
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ leadingCoeff (-p) = -leadingCoeff p
[PROOFSTEP]
rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]
[GOAL]
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ nextCoeff (↑C c) = 0
[PROOFSTEP]
rw [nextCoeff]
[GOAL]
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ (if natDegree (↑C c) = 0 then 0 else coeff (↑C c) (natDegree (↑C c) - 1)) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natDegree p
⊢ nextCoeff p = coeff p (natDegree p - 1)
[PROOFSTEP]
rw [nextCoeff, if_neg]
[GOAL]
case hnc
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natDegree p
⊢ ¬natDegree p = 0
[PROOFSTEP]
contrapose! hp
[GOAL]
case hnc
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p = 0
⊢ natDegree p ≤ 0
[PROOFSTEP]
simpa
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hpq : degree p ≤ degree q
hp : p ≠ 0
⊢ degree p ≠ ⊥
[PROOFSTEP]
rwa [Ne.def, Polynomial.degree_eq_bot]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : n < natDegree p
H : p = 0
⊢ False
[PROOFSTEP]
simp [H, Nat.not_lt_zero] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : natDegree p < natDegree q
⊢ degree p < degree q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : natDegree p < natDegree q
hp : p = 0
⊢ degree p < degree q
[PROOFSTEP]
simp [hp]
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : natDegree p < natDegree q
hp : p = 0
⊢ ⊥ < degree q
[PROOFSTEP]
rw [bot_lt_iff_ne_bot]
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : natDegree p < natDegree q
hp : p = 0
⊢ degree q ≠ ⊥
[PROOFSTEP]
intro hq
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : natDegree p < natDegree q
hp : p = 0
hq : degree q = ⊥
⊢ False
[PROOFSTEP]
simp [hp, degree_eq_bot.mp hq, lt_irrefl] at h
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : natDegree p < natDegree q
hp : ¬p = 0
⊢ degree p < degree q
[PROOFSTEP]
rwa [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h, Nat.cast_lt]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
h : degree p < degree q
⊢ natDegree p < natDegree q
[PROOFSTEP]
have hq : q ≠ 0 := ne_zero_of_degree_gt h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
h : degree p < degree q
hq : q ≠ 0
⊢ natDegree p < natDegree q
[PROOFSTEP]
rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p ≤ 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
ext (_ | n)
[GOAL]
case a.zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p ≤ 0
⊢ coeff p Nat.zero = coeff (↑C (coeff p 0)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case a.succ
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p ≤ 0
n : ℕ
⊢ coeff p (Nat.succ n) = coeff (↑C (coeff p 0)) (Nat.succ n)
[PROOFSTEP]
rw [coeff_C, if_neg (Nat.succ_ne_zero _), coeff_eq_zero_of_degree_lt]
[GOAL]
case a.succ
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p ≤ 0
n : ℕ
⊢ degree p < ↑(Nat.succ n)
[PROOFSTEP]
exact h.trans_lt (WithBot.some_lt_some.2 n.succ_pos)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ degree (p + q) ≤ max (degree p) (degree q)
[PROOFSTEP]
simpa only [degree, ← support_toFinsupp, toFinsupp_add] using AddMonoidAlgebra.sup_support_add_le _ _ _
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ natDegree (p + q) ≤ max (natDegree p) (natDegree q)
[PROOFSTEP]
cases' le_max_iff.1 (degree_add_le p q) with h h
[GOAL]
case inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
h : degree (p + q) ≤ degree p
⊢ natDegree (p + q) ≤ max (natDegree p) (natDegree q)
[PROOFSTEP]
simp [natDegree_le_natDegree h]
[GOAL]
case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
h : degree (p + q) ≤ degree q
⊢ natDegree (p + q) ≤ max (natDegree p) (natDegree q)
[PROOFSTEP]
simp [natDegree_le_natDegree h]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
⊢ leadingCoeff p ≠ 0 ↔ p ≠ 0
[PROOFSTEP]
rw [Ne.def, leadingCoeff_eq_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
⊢ leadingCoeff p = 0 ↔ degree p = ⊥
[PROOFSTEP]
rw [leadingCoeff_eq_zero, degree_eq_bot]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
H : p ≠ 0
⊢ natDegree p ∈ support p
[PROOFSTEP]
rw [mem_support_iff]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
H : p ≠ 0
⊢ coeff p (natDegree p) ≠ 0
[PROOFSTEP]
exact (not_congr leadingCoeff_eq_zero).mpr H
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree q < degree p
⊢ coeff (p + q) (natDegree p) ≠ 0
[PROOFSTEP]
rw [coeff_add, coeff_natDegree_eq_zero_of_degree_lt h, add_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree q < degree p
⊢ coeff p (natDegree p) ≠ 0
[PROOFSTEP]
exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p < degree q
⊢ degree (p + q) = degree q
[PROOFSTEP]
rw [add_comm, degree_add_eq_left_of_degree_lt h]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
⊢ natDegree (p + ↑C a) = natDegree p
[PROOFSTEP]
rcases eq_or_ne p 0 with rfl | hp
[GOAL]
case inl
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
q : R[X]
ι : Type u_1
a : R
⊢ natDegree (0 + ↑C a) = natDegree 0
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
hp : p ≠ 0
⊢ natDegree (p + ↑C a) = natDegree p
[PROOFSTEP]
by_cases hpd : p.degree ≤ 0
[GOAL]
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
hp : p ≠ 0
hpd : degree p ≤ 0
⊢ natDegree (p + ↑C a) = natDegree p
[PROOFSTEP]
rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
hp : p ≠ 0
hpd : ¬degree p ≤ 0
⊢ natDegree (p + ↑C a) = natDegree p
[PROOFSTEP]
rw [not_le, degree_eq_natDegree hp, Nat.cast_pos, ← natDegree_C a] at hpd
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
hp : p ≠ 0
hpd : natDegree (↑C a) < natDegree p
⊢ natDegree (p + ↑C a) = natDegree p
[PROOFSTEP]
exact natDegree_add_eq_left_of_natDegree_lt hpd
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
⊢ natDegree (↑C a + p) = natDegree p
[PROOFSTEP]
simp [add_comm _ p]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p + leadingCoeff q ≠ 0
hlt : degree p < degree q
⊢ max (degree p) (degree q) ≤ degree (p + q)
[PROOFSTEP]
rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p + leadingCoeff q ≠ 0
HEq : degree p = degree q
hlt : max (degree p) (degree q) > degree (p + q)
⊢ leadingCoeff p + leadingCoeff q = 0
[PROOFSTEP]
rw [HEq, max_self] at hlt
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p + leadingCoeff q ≠ 0
HEq : degree p = degree q
hlt : degree q > degree (p + q)
⊢ leadingCoeff p + leadingCoeff q = 0
[PROOFSTEP]
rw [leadingCoeff, leadingCoeff, natDegree_eq_of_degree_eq HEq, ← coeff_add]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p + leadingCoeff q ≠ 0
HEq : degree p = degree q
hlt : degree q > degree (p + q)
⊢ coeff (p + q) (natDegree q) = 0
[PROOFSTEP]
exact coeff_natDegree_eq_zero_of_degree_lt hlt
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p + leadingCoeff q ≠ 0
hlt : degree q < degree p
⊢ max (degree p) (degree q) ≤ degree (p + q)
[PROOFSTEP]
rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
⊢ degree (erase n p) ≤ degree p
[PROOFSTEP]
rcases p with ⟨p⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ degree (erase n { toFinsupp := p }) ≤ degree { toFinsupp := p }
[PROOFSTEP]
simp only [erase_def, degree, coeff, support]
  -- Porting note: simpler convert-free proof to be explicit about definition unfolding
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ Finset.max (Finsupp.erase n p).support ≤ Finset.max p.support
[PROOFSTEP]
apply sup_mono
[GOAL]
case ofFinsupp.h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (Finsupp.erase n p).support ⊆ p.support
[PROOFSTEP]
rw [Finsupp.support_erase]
[GOAL]
case ofFinsupp.h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ Finset.erase p.support n ⊆ p.support
[PROOFSTEP]
apply Finset.erase_subset
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
⊢ degree (erase (natDegree p) p) < degree p
[PROOFSTEP]
apply lt_of_le_of_ne (degree_erase_le _ _)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
⊢ degree (erase (natDegree p) p) ≠ degree p
[PROOFSTEP]
rw [degree_eq_natDegree hp, degree, support_erase]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
⊢ Finset.max (Finset.erase (support p) (natDegree p)) ≠ ↑(natDegree p)
[PROOFSTEP]
exact fun h => not_mem_erase _ _ (mem_of_max h)
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
a : R
⊢ degree (update p n a) ≤ max (degree p) ↑n
[PROOFSTEP]
rw [degree, support_update]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
a : R
⊢ Finset.max (if a = 0 then Finset.erase (support p) n else insert n (support p)) ≤ max (degree p) ↑n
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ Finset.max (Finset.erase (support p) n) ≤ max (degree p) ↑n
[PROOFSTEP]
exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ Finset.max (insert n (support p)) ≤ max (degree p) ↑n
[PROOFSTEP]
rw [max_insert, max_comm]
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ max (Finset.max (support p)) ↑n ≤ max (degree p) ↑n
[PROOFSTEP]
exact le_rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
s : Finset ι
f : ι → R[X]
⊢ degree (∑ i in ∅, f i) ≤ sup ∅ fun b => degree (f b)
[PROOFSTEP]
simp only [sum_empty, sup_empty, degree_zero, le_refl]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : ¬a ∈ s
ih : degree (∑ i in s, f i) ≤ sup s fun b => degree (f b)
⊢ degree (∑ i in insert a s, f i) ≤ max (degree (f a)) (degree (∑ i in s, f i))
[PROOFSTEP]
rw [sum_insert has]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : ¬a ∈ s
ih : degree (∑ i in s, f i) ≤ sup s fun b => degree (f b)
⊢ degree (f a + ∑ x in s, f x) ≤ max (degree (f a)) (degree (∑ i in s, f i))
[PROOFSTEP]
exact degree_add_le _ _
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : ¬a ∈ s
ih : degree (∑ i in s, f i) ≤ sup s fun b => degree (f b)
⊢ max (degree (f a)) (degree (∑ i in s, f i)) ≤ sup (insert a s) fun b => degree (f b)
[PROOFSTEP]
rw [sup_insert, sup_eq_max]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : ¬a ∈ s
ih : degree (∑ i in s, f i) ≤ sup s fun b => degree (f b)
⊢ max (degree (f a)) (degree (∑ i in s, f i)) ≤ max (degree (f a)) (sup s fun b => degree (f b))
[PROOFSTEP]
exact max_le_max le_rfl ih
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ degree (p * q) ≤ degree p + degree q
[PROOFSTEP]
simpa only [degree, ← support_toFinsupp, toFinsupp_mul] using
  AddMonoidAlgebra.sup_support_mul_le (WithBot.coe_add _ _).le _ _
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
⊢ degree (p ^ 0) ≤ 0 • degree p
[PROOFSTEP]
rw [pow_zero, zero_nsmul]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
⊢ degree 1 ≤ 0
[PROOFSTEP]
exact degree_one_le
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
⊢ degree (p ^ (n + 1)) ≤ degree p + degree (p ^ n)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
⊢ degree (p * p ^ n) ≤ degree p + degree (p ^ n)
[PROOFSTEP]
exact degree_mul_le _ _
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
⊢ degree p + degree (p ^ n) ≤ (n + 1) • degree p
[PROOFSTEP]
rw [succ_nsmul]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
⊢ degree p + degree (p ^ n) ≤ degree p + n • degree p
[PROOFSTEP]
exact add_le_add le_rfl (degree_pow_le _ _)
[GOAL]
R : Type u
S : Type v
a✝ b✝ c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : WithBot ℕ
b : ℕ
hp : degree p ≤ a
⊢ degree (p ^ b) ≤ ↑b * a
[PROOFSTEP]
induction b with
| zero => simp [degree_one_le]
| succ n hn =>
  rw [Nat.cast_succ, add_mul, one_mul, pow_succ']
  exact degree_mul_le_of_le hn hp
[GOAL]
R : Type u
S : Type v
a✝ b✝ c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : WithBot ℕ
b : ℕ
hp : degree p ≤ a
⊢ degree (p ^ b) ≤ ↑b * a
[PROOFSTEP]
induction b with
| zero => simp [degree_one_le]
| succ n hn =>
  rw [Nat.cast_succ, add_mul, one_mul, pow_succ']
  exact degree_mul_le_of_le hn hp
[GOAL]
case zero
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : WithBot ℕ
hp : degree p ≤ a
⊢ degree (p ^ Nat.zero) ≤ ↑Nat.zero * a
[PROOFSTEP]

| zero => simp [degree_one_le]
[GOAL]
case zero
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : WithBot ℕ
hp : degree p ≤ a
⊢ degree (p ^ Nat.zero) ≤ ↑Nat.zero * a
[PROOFSTEP]
simp [degree_one_le]
[GOAL]
case succ
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : WithBot ℕ
hp : degree p ≤ a
n : ℕ
hn : degree (p ^ n) ≤ ↑n * a
⊢ degree (p ^ Nat.succ n) ≤ ↑(Nat.succ n) * a
[PROOFSTEP]

| succ n hn =>
  rw [Nat.cast_succ, add_mul, one_mul, pow_succ']
  exact degree_mul_le_of_le hn hp
[GOAL]
case succ
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : WithBot ℕ
hp : degree p ≤ a
n : ℕ
hn : degree (p ^ n) ≤ ↑n * a
⊢ degree (p ^ Nat.succ n) ≤ ↑(Nat.succ n) * a
[PROOFSTEP]
rw [Nat.cast_succ, add_mul, one_mul, pow_succ']
[GOAL]
case succ
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : WithBot ℕ
hp : degree p ≤ a
n : ℕ
hn : degree (p ^ n) ≤ ↑n * a
⊢ degree (p ^ n * p) ≤ ↑n * a + a
[PROOFSTEP]
exact degree_mul_le_of_le hn hp
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
n : ℕ
⊢ leadingCoeff (↑(monomial n) a) = a
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
n : ℕ
ha : a = 0
⊢ leadingCoeff (↑(monomial n) a) = a
[PROOFSTEP]
simp only [ha, (monomial n).map_zero, leadingCoeff_zero]
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
n : ℕ
ha : ¬a = 0
⊢ leadingCoeff (↑(monomial n) a) = a
[PROOFSTEP]
rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
n : ℕ
ha : ¬a = 0
⊢ (if n = n then a else 0) = a
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
n : ℕ
⊢ leadingCoeff (↑C a * X ^ n) = a
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
a : R
⊢ leadingCoeff (↑C a * X) = a
[PROOFSTEP]
simpa only [pow_one] using leadingCoeff_C_mul_X_pow a 1
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
⊢ leadingCoeff (X ^ n) = 1
[PROOFSTEP]
simpa only [C_1, one_mul] using leadingCoeff_C_mul_X_pow (1 : R) n
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
⊢ leadingCoeff X = 1
[PROOFSTEP]
simpa only [pow_one] using @leadingCoeff_X_pow R _ 1
[GOAL]
R✝ : Type u
S : Type v
a b c d : R✝
n m : ℕ
inst✝² : Semiring R✝
p✝ q : R✝[X]
ι : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : Monic p
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R✝ : Type u
S : Type v
a b c d : R✝
n m : ℕ
inst✝² : Semiring R✝
p q : R✝[X]
ι : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hp : Monic 0
⊢ False
[PROOFSTEP]
simp [Monic] at hp
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
h : 0 ≠ 1
p : R[X]
hp : Monic p
⊢ p ≠ 0
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
ι : Type u_1
h : 0 ≠ 1
p : R[X]
hp : Monic p
inst✝ : Nontrivial R
⊢ p ≠ 0
[PROOFSTEP]
exact hp.ne_zero
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
⊢ Monic p
[PROOFSTEP]
unfold Monic
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
⊢ leadingCoeff p = 1
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
✝ : Nontrivial R
⊢ leadingCoeff p = 1
[PROOFSTEP]
refine' (congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn _).trans p1
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
pn : natDegree p ≤ n
p1 : coeff p n = 1
✝ : Nontrivial R
⊢ coeff p n ≠ 0
[PROOFSTEP]
exact ne_of_eq_of_ne p1 one_ne_zero
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p < degree q
⊢ leadingCoeff (p + q) = leadingCoeff q
[PROOFSTEP]
have : coeff p (natDegree q) = 0 := coeff_natDegree_eq_zero_of_degree_lt h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p < degree q
this : coeff p (natDegree q) = 0
⊢ leadingCoeff (p + q) = leadingCoeff q
[PROOFSTEP]
simp only [leadingCoeff, natDegree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h), this, coeff_add, zero_add]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree q < degree p
⊢ leadingCoeff (p + q) = leadingCoeff p
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree q < degree p
⊢ leadingCoeff (q + p) = leadingCoeff p
[PROOFSTEP]
exact leadingCoeff_add_of_degree_lt h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
⊢ leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q
[PROOFSTEP]
have : natDegree (p + q) = natDegree p := by
  apply natDegree_eq_of_degree_eq
  rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
⊢ natDegree (p + q) = natDegree p
[PROOFSTEP]
apply natDegree_eq_of_degree_eq
[GOAL]
case h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
⊢ degree (p + q) = degree p
[PROOFSTEP]
rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
this : natDegree (p + q) = natDegree p
⊢ leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q
[PROOFSTEP]
simp only [leadingCoeff, this, natDegree_eq_of_degree_eq h, coeff_add]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ ∑ x in Nat.antidiagonal (natDegree p + natDegree q), coeff p x.fst * coeff q x.snd =
    coeff p (natDegree p) * coeff q (natDegree q)
[PROOFSTEP]
refine' Finset.sum_eq_single (natDegree p, natDegree q) _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ ∀ (b : ℕ × ℕ),
    b ∈ Nat.antidiagonal (natDegree p + natDegree q) →
      b ≠ (natDegree p, natDegree q) → coeff p b.fst * coeff q b.snd = 0
[PROOFSTEP]
rintro ⟨i, j⟩ h₁ h₂
[GOAL]
case refine'_1.mk
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ Nat.antidiagonal (natDegree p + natDegree q)
h₂ : (i, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [Nat.mem_antidiagonal] at h₁
[GOAL]
case refine'_1.mk
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
by_cases H : natDegree p < i
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p < i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_degree_lt (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)), zero_mul]
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : ¬natDegree p < i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [not_lt_iff_eq_or_lt] at H
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p = i ∨ i < natDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
cases' H with H H
[GOAL]
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p = i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
subst H
[GOAL]
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
j : ℕ
h₁ : (natDegree p, j).fst + (natDegree p, j).snd = natDegree p + natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
[PROOFSTEP]
rw [add_left_cancel_iff] at h₁
[GOAL]
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
j : ℕ
h₁ : (natDegree p, j).snd = natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
[PROOFSTEP]
dsimp at h₁
[GOAL]
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
j : ℕ
h₁ : j = natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
[PROOFSTEP]
subst h₁
[GOAL]
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
h₂ : (natDegree p, natDegree q) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
[PROOFSTEP]
exact (h₂ rfl).elim
[GOAL]
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
suffices natDegree q < j by
  rw [coeff_eq_zero_of_degree_lt (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)), mul_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
this : natDegree q < j
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_degree_lt (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)), mul_zero]
[GOAL]
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
⊢ natDegree q < j
[PROOFSTEP]
by_contra' H'
[GOAL]
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
H' : j ≤ natDegree q
⊢ False
[PROOFSTEP]
exact ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _)) h₁
[GOAL]
case refine'_2
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q) →
    coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
[PROOFSTEP]
intro H
[GOAL]
case refine'_2
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
[PROOFSTEP]
exfalso
[GOAL]
case refine'_2.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ False
[PROOFSTEP]
apply H
[GOAL]
case refine'_2.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ (natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
[PROOFSTEP]
rw [Nat.mem_antidiagonal]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ p ≠ 0
[PROOFSTEP]
refine' mt _ h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ p = 0 → leadingCoeff p * leadingCoeff q = 0
[PROOFSTEP]
exact fun hp => by rw [hp, leadingCoeff_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p = 0
⊢ leadingCoeff p * leadingCoeff q = 0
[PROOFSTEP]
rw [hp, leadingCoeff_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
⊢ q ≠ 0
[PROOFSTEP]
refine' mt _ h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
⊢ q = 0 → leadingCoeff p * leadingCoeff q = 0
[PROOFSTEP]
exact fun hq => by rw [hq, leadingCoeff_zero, mul_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ leadingCoeff p * leadingCoeff q = 0
[PROOFSTEP]
rw [hq, leadingCoeff_zero, mul_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ degree p + degree q ≤ degree (p * q)
[PROOFSTEP]
rw [degree_eq_natDegree hp, degree_eq_natDegree hq]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑(natDegree p) + ↑(natDegree q) ≤ degree (p * q)
[PROOFSTEP]
refine le_degree_of_ne_zero (n := natDegree p + natDegree q) ?_
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ coeff (p * q) (natDegree p + natDegree q) ≠ 0
[PROOFSTEP]
rwa [coeff_mul_degree_add_degree]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hq : Monic q
hp : p = 0
⊢ degree (p * q) = degree p + degree q
[PROOFSTEP]
simp [hp]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hq : Monic q
hp : ¬p = 0
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
rwa [hq.leadingCoeff, mul_one, Ne.def, leadingCoeff_eq_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
h₁ : leadingCoeff p = 0
⊢ leadingCoeff p * leadingCoeff q = 0
[PROOFSTEP]
rw [h₁, zero_mul]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
h₁ : leadingCoeff q = 0
⊢ leadingCoeff p * leadingCoeff q = 0
[PROOFSTEP]
rw [h₁, mul_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ degree (p * q) = ↑(natDegree p + natDegree q)
[PROOFSTEP]
rw [degree_mul' h, Nat.cast_add, degree_eq_natDegree hp, degree_eq_natDegree hq]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
[PROOFSTEP]
unfold leadingCoeff
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ coeff (p * q) (natDegree (p * q)) = coeff p (natDegree p) * coeff q (natDegree q)
[PROOFSTEP]
rw [natDegree_mul' h, coeff_mul_degree_add_degree]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p * leadingCoeff q ≠ 0
⊢ leadingCoeff p * leadingCoeff q = coeff p (natDegree p) * coeff q (natDegree q)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : card (support p) ≤ 1
⊢ ↑(monomial (natDegree p)) (leadingCoeff p) = p
[PROOFSTEP]
rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
q : R[X]
ι : Type u_1
n : ℕ
a : R
h : card (support (↑(monomial n) a)) ≤ 1
⊢ ↑(monomial (natDegree (↑(monomial n) a))) (leadingCoeff (↑(monomial n) a)) = ↑(monomial n) a
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
q : R[X]
ι : Type u_1
n : ℕ
a : R
h : card (support (↑(monomial n) a)) ≤ 1
ha : a = 0
⊢ ↑(monomial (natDegree (↑(monomial n) a))) (leadingCoeff (↑(monomial n) a)) = ↑(monomial n) a
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
q : R[X]
ι : Type u_1
n : ℕ
a : R
h : card (support (↑(monomial n) a)) ≤ 1
ha : ¬a = 0
⊢ ↑(monomial (natDegree (↑(monomial n) a))) (leadingCoeff (↑(monomial n) a)) = ↑(monomial n) a
[PROOFSTEP]
simp [ha]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : card (support p) ≤ 1
⊢ ↑C (leadingCoeff p) * X ^ natDegree p = p
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
⊢ leadingCoeff p ^ Nat.zero ≠ 0 → leadingCoeff (p ^ Nat.zero) = leadingCoeff p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
⊢ leadingCoeff (p ^ Nat.succ n) = leadingCoeff p ^ Nat.succ n
[PROOFSTEP]
have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, mul_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n = 0
⊢ leadingCoeff p ^ Nat.succ n = 0
[PROOFSTEP]
rw [pow_succ, h₁, mul_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
⊢ leadingCoeff (p ^ Nat.succ n) = leadingCoeff p ^ Nat.succ n
[PROOFSTEP]
have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ, ← ih h₁] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
⊢ leadingCoeff p * leadingCoeff (p ^ n) ≠ 0
[PROOFSTEP]
rwa [pow_succ, ← ih h₁] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0
⊢ leadingCoeff (p ^ Nat.succ n) = leadingCoeff p ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, pow_succ, leadingCoeff_mul' h₂, ih h₁]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : leadingCoeff p ^ 0 ≠ 0
⊢ degree (p ^ 0) = 0 • degree p
[PROOFSTEP]
rw [pow_zero, ← C_1] at *
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : 1 ≠ 0
⊢ degree (↑C 1) = 0 • degree p
[PROOFSTEP]
rw [degree_C h, zero_nsmul]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ (n + 1) ≠ 0
⊢ degree (p ^ (n + 1)) = (n + 1) • degree p
[PROOFSTEP]
have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, mul_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ (n + 1) ≠ 0
h₁ : leadingCoeff p ^ n = 0
⊢ leadingCoeff p ^ (n + 1) = 0
[PROOFSTEP]
rw [pow_succ, h₁, mul_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ (n + 1) ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
⊢ degree (p ^ (n + 1)) = (n + 1) • degree p
[PROOFSTEP]
have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ (n + 1) ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
⊢ leadingCoeff p * leadingCoeff (p ^ n) ≠ 0
[PROOFSTEP]
rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ (n + 1) ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0
⊢ degree (p ^ (n + 1)) = (n + 1) • degree p
[PROOFSTEP]
rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : p = 0
hn0 : n = 0
⊢ natDegree (p ^ n) = n * natDegree p
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree (p ^ n) = n * natDegree p
[PROOFSTEP]
rw [hp0, zero_pow (Nat.pos_of_ne_zero hn0)]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree 0 = n * natDegree 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn0 : p ^ n = 0
⊢ False
[PROOFSTEP]
have h1 := h
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : leadingCoeff p ^ n ≠ 0
⊢ False
[PROOFSTEP]
rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : 0 ≠ 0
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : leadingCoeff p ^ n ≠ 0
⊢ False
[PROOFSTEP]
exact h rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ ↑(natDegree (p ^ n)) = ↑(n * natDegree p)
[PROOFSTEP]
rw [← degree_eq_natDegree hpn, degree_pow' h, degree_eq_natDegree hp0]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ
h : leadingCoeff p ^ n ≠ 0
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ n • ↑(natDegree p) = ↑(n * natDegree p)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
hp : Monic p
⊢ leadingCoeff (p * q) = leadingCoeff q
[PROOFSTEP]
rcases eq_or_ne q 0 with (rfl | H)
[GOAL]
case inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
hp : Monic p
⊢ leadingCoeff (p * 0) = leadingCoeff 0
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
hp : Monic p
H : q ≠ 0
⊢ leadingCoeff (p * q) = leadingCoeff q
[PROOFSTEP]
rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]
[GOAL]
case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
hp : Monic p
H : q ≠ 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
[PROOFSTEP]
rwa [hp.leadingCoeff, one_mul, Ne.def, leadingCoeff_eq_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
hq : Monic q
H : leadingCoeff p = 0
⊢ leadingCoeff (p * q) = leadingCoeff p
[PROOFSTEP]
rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
hq : Monic q
H : leadingCoeff p ≠ 0
⊢ leadingCoeff (p * q) = leadingCoeff p
[PROOFSTEP]
rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
hq : Monic q
H : leadingCoeff p ≠ 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
[PROOFSTEP]
rwa [hq.leadingCoeff, mul_one]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ natDegree (p * q) ≤ natDegree p + natDegree q
[PROOFSTEP]
apply natDegree_le_of_degree_le
[GOAL]
case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ degree (p * q) ≤ ↑(natDegree p + natDegree q)
[PROOFSTEP]
apply le_trans (degree_mul_le p q)
[GOAL]
case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ degree p + degree q ≤ ↑(natDegree p + natDegree q)
[PROOFSTEP]
rw [Nat.cast_add]
[GOAL]
case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ degree p + degree q ≤ ↑(natDegree p) + ↑(natDegree q)
[PROOFSTEP]
apply add_le_add
[GOAL]
case a.h₁
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ degree p ≤ ↑(natDegree p)
[PROOFSTEP]
apply degree_le_natDegree
[GOAL]
case a.h₂
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type u_1
p q : R[X]
⊢ degree q ≤ ↑(natDegree q)
[PROOFSTEP]
apply degree_le_natDegree
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
⊢ natDegree (p ^ n) ≤ n * natDegree p
[PROOFSTEP]
induction' n with i hi
[GOAL]
case zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
⊢ natDegree (p ^ Nat.zero) ≤ Nat.zero * natDegree p
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree (p ^ Nat.succ i) ≤ Nat.succ i * natDegree p
[PROOFSTEP]
rw [pow_succ, Nat.succ_mul, add_comm]
[GOAL]
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree (p * p ^ i) ≤ natDegree p + i * natDegree p
[PROOFSTEP]
apply le_trans natDegree_mul_le
[GOAL]
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree p + natDegree (p ^ i) ≤ natDegree p + i * natDegree p
[PROOFSTEP]
exact add_le_add_left hi _
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
n : ℕ
⊢ coeff (p ^ n) (n * natDegree p) = leadingCoeff p ^ n
[PROOFSTEP]
induction' n with i hi
[GOAL]
case zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
⊢ coeff (p ^ Nat.zero) (Nat.zero * natDegree p) = leadingCoeff p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
⊢ coeff (p ^ Nat.succ i) (Nat.succ i * natDegree p) = leadingCoeff p ^ Nat.succ i
[PROOFSTEP]
rw [pow_succ', pow_succ', Nat.succ_mul]
[GOAL]
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p
[PROOFSTEP]
by_cases hp1 : p.leadingCoeff ^ i = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p
[PROOFSTEP]
rw [hp1, zero_mul]
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0
[PROOFSTEP]
by_cases hp2 : p ^ i = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0
[PROOFSTEP]
rw [hp2, zero_mul, coeff_zero]
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = 0
[PROOFSTEP]
apply coeff_eq_zero_of_natDegree_lt
[GOAL]
case neg.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
⊢ natDegree (p ^ i * p) < i * natDegree p + natDegree p
[PROOFSTEP]
have h1 : (p ^ i).natDegree < i * p.natDegree :=
  by
  refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
  rw [← h, hp1] at hi
  exact leadingCoeff_eq_zero.mp hi
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
⊢ natDegree (p ^ i) < i * natDegree p
[PROOFSTEP]
refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h : natDegree (p ^ i) = i * natDegree p
⊢ p ^ i = 0
[PROOFSTEP]
rw [← h, hp1] at hi
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (natDegree (p ^ i)) = 0
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h : natDegree (p ^ i) = i * natDegree p
⊢ p ^ i = 0
[PROOFSTEP]
exact leadingCoeff_eq_zero.mp hi
[GOAL]
case neg.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : leadingCoeff p ^ i = 0
hp2 : ¬p ^ i = 0
h1 : natDegree (p ^ i) < i * natDegree p
⊢ natDegree (p ^ i * p) < i * natDegree p + natDegree p
[PROOFSTEP]
calc
  (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
  _ < i * p.natDegree + p.natDegree := add_lt_add_right h1 _
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : ¬leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (i * natDegree p + natDegree p) = leadingCoeff p ^ i * leadingCoeff p
[PROOFSTEP]
rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
p : R[X]
i : ℕ
hi : coeff (p ^ i) (i * natDegree p) = leadingCoeff p ^ i
hp1 : ¬leadingCoeff p ^ i = 0
⊢ coeff (p ^ i * p) (natDegree (p ^ i) + natDegree p) = leadingCoeff (p ^ i) * leadingCoeff p
[PROOFSTEP]
exact coeff_mul_degree_add_degree _ _
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
⊢ coeff (f * g) (df + dg) = coeff f df * coeff g dg
[PROOFSTEP]
rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)]
[GOAL]
case h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
⊢ (df, dg) ∈ Nat.antidiagonal (df + dg)
[PROOFSTEP]
rw [Finset.Nat.mem_antidiagonal]
[GOAL]
case h₀
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
⊢ ∀ (b : ℕ × ℕ), b ∈ Nat.antidiagonal (df + dg) → b ≠ (df, dg) → coeff f b.fst * coeff g b.snd = 0
[PROOFSTEP]
rintro ⟨df', dg'⟩ hmem hne
[GOAL]
case h₀.mk
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ Nat.antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
⊢ coeff f (df', dg').fst * coeff g (df', dg').snd = 0
[PROOFSTEP]
obtain h | hdf' := lt_or_le df df'
[GOAL]
case h₀.mk.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ Nat.antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
h : df < df'
⊢ coeff f (df', dg').fst * coeff g (df', dg').snd = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul]
[GOAL]
case h₀.mk.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ Nat.antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
⊢ coeff f (df', dg').fst * coeff g (df', dg').snd = 0
[PROOFSTEP]
obtain h | hdg' := lt_or_le dg dg'
[GOAL]
case h₀.mk.inr.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ Nat.antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h : dg < dg'
⊢ coeff f (df', dg').fst * coeff g (df', dg').snd = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]
[GOAL]
case h₀.mk.inr.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ Nat.antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
⊢ coeff f (df', dg').fst * coeff g (df', dg').snd = 0
[PROOFSTEP]
obtain ⟨rfl, rfl⟩ := eq_and_eq_of_le_of_le_of_add_le hdf' hdg' (Finset.Nat.mem_antidiagonal.1 hmem).ge
[GOAL]
case h₀.mk.inr.inr.intro
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
df dg : ℕ
g : R[X]
hdf : natDegree f ≤ df
hdg : natDegree g ≤ dg
hdf' : df ≤ df
hdg' : dg ≤ dg
hmem : (df, dg) ∈ Nat.antidiagonal (df + dg)
hne : (df, dg) ≠ (df, dg)
⊢ coeff f (df, dg).fst * coeff g (df, dg).snd = 0
[PROOFSTEP]
exact (hne rfl).elim
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
⊢ 0 ≤ degree p ↔ p ≠ 0
[PROOFSTEP]
rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
⊢ natDegree p = 0 ↔ degree p ≤ 0
[PROOFSTEP]
rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le, Nat.cast_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
n : WithBot ℕ
⊢ degree f ≤ n ↔ ∀ (m : ℕ), n < ↑m → coeff f m = 0
[PROOFSTEP]
simp only [degree, Finset.max, Finset.sup_le_iff, mem_support_iff, Ne.def, ← not_le, not_imp_comm, Nat.cast_withBot]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
f : R[X]
n : ℕ
⊢ degree f < ↑n ↔ ∀ (m : ℕ), n ≤ m → coeff f m = 0
[PROOFSTEP]
simp only [degree, Finset.sup_lt_iff (WithBot.bot_lt_coe n), mem_support_iff, WithBot.coe_lt_coe, ← @not_le ℕ,
  max_eq_sup_coe, Nat.cast_withBot, Ne.def, not_imp_not]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
a : R
p : R[X]
⊢ degree (a • p) ≤ degree p
[PROOFSTEP]
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
a : R
p : R[X]
m : ℕ
hm : degree p < ↑m
⊢ coeff (a • p) m = 0
[PROOFSTEP]
rw [degree_lt_iff_coeff_zero] at hm
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type u_1
a : R
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff p m_1 = 0
⊢ coeff (a • p) m = 0
[PROOFSTEP]
simp [hm m le_rfl]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
⊢ degree p < degree (p * X)
[PROOFSTEP]
haveI := Nontrivial.of_polynomial_ne hp
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
this : Nontrivial R
⊢ degree p < degree (p * X)
[PROOFSTEP]
have : leadingCoeff p * leadingCoeff X ≠ 0 := by simpa
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
this : Nontrivial R
⊢ leadingCoeff p * leadingCoeff X ≠ 0
[PROOFSTEP]
simpa
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
this✝ : Nontrivial R
this : leadingCoeff p * leadingCoeff X ≠ 0
⊢ degree p < degree (p * X)
[PROOFSTEP]
erw [degree_mul' this, degree_eq_natDegree hp, degree_X, ← WithBot.coe_one, ← WithBot.coe_add, WithBot.coe_lt_coe]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hp : p ≠ 0
this✝ : Nontrivial R
this : leadingCoeff p * leadingCoeff X ≠ 0
⊢ ↑(natDegree p) < ↑(natDegree p) + 1
[PROOFSTEP]
exact Nat.lt_succ_self _
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
h : p = ↑C (coeff p 0)
⊢ natDegree p = 0
[PROOFSTEP]
rw [h, natDegree_C]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
hdeg : ↑n ≤ degree p
⊢ ↑n ≤ ↑(natDegree p)
[PROOFSTEP]
rwa [degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg] at hdeg
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ degree (↑C b) < degree (↑C a * X)
[PROOFSTEP]
simpa only [degree_C_mul_X ha] using degree_C_lt
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ degree (↑C a * X + ↑C b) = 1
[PROOFSTEP]
rw [degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha, degree_C_mul_X ha]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ natDegree (↑C a * X + ↑C b) = 1
[PROOFSTEP]
rw [natDegree_add_C, natDegree_C_mul_X a ha]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ leadingCoeff (↑C a * X + ↑C b) = a
[PROOFSTEP]
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_lt_degree_C_mul_X ha), leadingCoeff_C_mul_X]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
⊢ degree (↑C a * X ^ 2 + ↑C b * X + ↑C c) ≤ 2
[PROOFSTEP]
simpa only [add_assoc] using
  degree_add_le_of_degree_le (degree_C_mul_X_pow_le 2 a)
    (le_trans degree_linear_le <| WithBot.coe_le_coe.mpr one_le_two)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ degree (↑C b * X + ↑C c) < degree (↑C a * X ^ 2)
[PROOFSTEP]
simpa only [degree_C_mul_X_pow 2 ha] using degree_linear_lt
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ degree (↑C a * X ^ 2 + ↑C b * X + ↑C c) = 2
[PROOFSTEP]
rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha, degree_C_mul_X_pow 2 ha]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ ↑2 = 2
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ leadingCoeff (↑C a * X ^ 2 + ↑C b * X + ↑C c) = a
[PROOFSTEP]
rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
  leadingCoeff_C_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
⊢ degree (↑C a * X ^ 3 + ↑C b * X ^ 2 + ↑C c * X + ↑C d) ≤ 3
[PROOFSTEP]
simpa only [add_assoc] using
  degree_add_le_of_degree_le (degree_C_mul_X_pow_le 3 a)
    (le_trans degree_quadratic_le <| WithBot.coe_le_coe.mpr <| Nat.le_succ 2)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ degree (↑C b * X ^ 2 + ↑C c * X + ↑C d) < degree (↑C a * X ^ 3)
[PROOFSTEP]
simpa only [degree_C_mul_X_pow 3 ha] using degree_quadratic_lt
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ degree (↑C a * X ^ 3 + ↑C b * X ^ 2 + ↑C c * X + ↑C d) = 3
[PROOFSTEP]
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2),
  degree_add_eq_left_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha, degree_C_mul_X_pow 3 ha]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ ↑3 = 3
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
ha : a ≠ 0
⊢ leadingCoeff (↑C a * X ^ 3 + ↑C b * X ^ 2 + ↑C c * X + ↑C d) = a
[PROOFSTEP]
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
  leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha, leadingCoeff_C_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p q : R[X]
n : ℕ
⊢ degree (X ^ n) = ↑n
[PROOFSTEP]
rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]
[GOAL]
R✝ : Type u
S : Type v
a b c d : R✝
n✝ m : ℕ
inst✝² : Semiring R✝
inst✝¹ : Nontrivial R✝
p q : R✝[X]
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ natDegree (X ^ n) ≤ n
[PROOFSTEP]
nontriviality R
[GOAL]
R✝ : Type u
S : Type v
a b c d : R✝
n✝ m : ℕ
inst✝² : Semiring R✝
inst✝¹ : Nontrivial R✝
p q : R✝[X]
R : Type u_1
inst✝ : Semiring R
n : ℕ
✝ : Nontrivial R
⊢ natDegree (X ^ n) ≤ n
[PROOFSTEP]
rw [Polynomial.natDegree_X_pow]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p q : R[X]
x✝ : IsUnit X
g : R[X]
_hfg : ↑(monomial 1) 1 * g = 1
hgf : g * ↑(monomial 1) 1 = 1
⊢ 0 = 1
[PROOFSTEP]
rw [← coeff_one_zero, ← hgf]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p q : R[X]
x✝ : IsUnit X
g : R[X]
_hfg : ↑(monomial 1) 1 * g = 1
hgf : g * ↑(monomial 1) 1 = 1
⊢ 0 = coeff (g * ↑(monomial 1) 1) 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p q : R[X]
⊢ degree (p * X) = degree p + 1
[PROOFSTEP]
simp [monic_X.degree_mul]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p q : R[X]
⊢ degree (p * X ^ n) = degree p + ↑n
[PROOFSTEP]
simp [(monic_X_pow n).degree_mul]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p✝ q✝ p q : R[X]
⊢ degree (p - q) ≤ max (degree p) (degree q)
[PROOFSTEP]
simpa only [degree_neg q] using degree_add_le p (-q)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q < degree p
⊢ leadingCoeff (p - q) = leadingCoeff p
[PROOFSTEP]
rw [← q.degree_neg] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree (-q) < degree p
⊢ leadingCoeff (p - q) = leadingCoeff p
[PROOFSTEP]
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt' h]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p < degree q
⊢ leadingCoeff (p - q) = -leadingCoeff q
[PROOFSTEP]
rw [← q.degree_neg] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p < degree (-q)
⊢ leadingCoeff (p - q) = -leadingCoeff q
[PROOFSTEP]
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p = degree q
hlc : leadingCoeff p ≠ leadingCoeff q
⊢ leadingCoeff (p - q) = leadingCoeff p - leadingCoeff q
[PROOFSTEP]
replace h : degree p = degree (-q) := by rwa [q.degree_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p = degree q
hlc : leadingCoeff p ≠ leadingCoeff q
⊢ degree p = degree (-q)
[PROOFSTEP]
rwa [q.degree_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hlc : leadingCoeff p ≠ leadingCoeff q
h : degree p = degree (-q)
⊢ leadingCoeff (p - q) = leadingCoeff p - leadingCoeff q
[PROOFSTEP]
replace hlc : leadingCoeff p + leadingCoeff (-q) ≠ 0 := by
  rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hlc : leadingCoeff p ≠ leadingCoeff q
h : degree p = degree (-q)
⊢ leadingCoeff p + leadingCoeff (-q) ≠ 0
[PROOFSTEP]
rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p = degree (-q)
hlc : leadingCoeff p + leadingCoeff (-q) ≠ 0
⊢ leadingCoeff (p - q) = leadingCoeff p - leadingCoeff q
[PROOFSTEP]
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p✝ q✝ p q : R[X]
⊢ natDegree (p - q) ≤ max (natDegree p) (natDegree q)
[PROOFSTEP]
simpa only [← natDegree_neg q] using natDegree_add_le p (-q)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
⊢ natDegree p = natDegree q
[PROOFSTEP]
unfold natDegree
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
⊢ WithBot.unbot' 0 (degree p) = WithBot.unbot' 0 (degree q)
[PROOFSTEP]
rw [hd]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
hd' : natDegree p = natDegree q
hq0 : q ≠ 0
⊢ degree (p - q) = degree (erase (natDegree q) p + -erase (natDegree q) q)
[PROOFSTEP]
conv =>
  lhs
  rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
hd' : natDegree p = natDegree q
hq0 : q ≠ 0
| degree (p - q) = degree (erase (natDegree q) p + -erase (natDegree q) q)
[PROOFSTEP]
  lhs
  rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
hd' : natDegree p = natDegree q
hq0 : q ≠ 0
| degree (p - q) = degree (erase (natDegree q) p + -erase (natDegree q) q)
[PROOFSTEP]
  lhs
  rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
hd' : natDegree p = natDegree q
hq0 : q ≠ 0
| degree (p - q) = degree (erase (natDegree q) p + -erase (natDegree q) q)
[PROOFSTEP]
lhs
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
hd' : natDegree p = natDegree q
hq0 : q ≠ 0
| degree (p - q)
[PROOFSTEP]
rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q < degree p
⊢ degree (p - q) = degree p
[PROOFSTEP]
rw [← degree_neg q] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree (-q) < degree p
⊢ degree (p - q) = degree p
[PROOFSTEP]
rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p < degree q
⊢ degree (p - q) = degree q
[PROOFSTEP]
rw [← degree_neg q] at h
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p < degree (-q)
⊢ degree (p - q) = degree q
[PROOFSTEP]
rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
⊢ degree (X + ↑C a) = 1
[PROOFSTEP]
have : degree (C a) < degree (X : R[X]) :=
  calc
    degree (C a) ≤ 0 := degree_C_le
    _ < 1 := (WithBot.some_lt_some.mpr zero_lt_one)
    _ = degree X := degree_X.symm
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : degree (↑C a) < degree X
⊢ degree (X + ↑C a) = 1
[PROOFSTEP]
rw [degree_add_eq_left_of_degree_lt this, degree_X]
[GOAL]
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝² : Nontrivial R
inst✝¹ : Semiring R
inst✝ : Semiring S
c : S
⊢ nextCoeff (X + ↑C c) = c
[PROOFSTEP]
nontriviality S
[GOAL]
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝² : Nontrivial R
inst✝¹ : Semiring R
inst✝ : Semiring S
c : S
✝ : Nontrivial S
⊢ nextCoeff (X + ↑C c) = c
[PROOFSTEP]
simp [nextCoeff_of_pos_natDegree]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ degree (X ^ n + ↑C a) = ↑n
[PROOFSTEP]
have : degree (C a) < degree ((X : R[X]) ^ n) := degree_C_le.trans_lt <| by rwa [degree_X_pow, Nat.cast_pos]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < degree (X ^ n)
[PROOFSTEP]
rwa [degree_X_pow, Nat.cast_pos]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
this : degree (↑C a) < degree (X ^ n)
⊢ degree (X ^ n + ↑C a) = ↑n
[PROOFSTEP]
rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ degree (X ^ n + ↑C a) ≠ ⊥
[PROOFSTEP]
rw [degree_X_pow_add_C hn a]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ ↑n ≠ ⊥
[PROOFSTEP]
exact WithBot.coe_ne_bot
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
⊢ natDegree (X ^ n + ↑C r) = n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : n = 0
⊢ natDegree (X ^ n + ↑C r) = n
[PROOFSTEP]
rw [hn, pow_zero, ← C_1, ← RingHom.map_add, natDegree_C]
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : ¬n = 0
⊢ natDegree (X ^ n + ↑C r) = n
[PROOFSTEP]
exact natDegree_eq_of_degree_eq_some (degree_X_pow_add_C (pos_iff_ne_zero.mpr hn) r)
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
h : X ^ n + ↑C a = 1
⊢ n = 0
[PROOFSTEP]
simpa only [natDegree_X_pow_add_C, natDegree_one] using congr_arg natDegree h
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
⊢ leadingCoeff (X ^ n + ↑C r) = 1
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
✝ : Nontrivial R
⊢ leadingCoeff (X ^ n + ↑C r) = 1
[PROOFSTEP]
rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C, if_neg (pos_iff_ne_zero.mp hn), add_zero]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
r : S
⊢ leadingCoeff (X + ↑C r) = 1
[PROOFSTEP]
rw [← pow_one (X : S[X]), leadingCoeff_X_pow_add_C zero_lt_one]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
r : R
i : ℕ
⊢ leadingCoeff ((X + ↑C r) ^ i) = 1
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
r : R
i : ℕ
✝ : Nontrivial R
⊢ leadingCoeff ((X + ↑C r) ^ i) = 1
[PROOFSTEP]
rw [leadingCoeff_pow']
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
r : R
i : ℕ
✝ : Nontrivial R
⊢ leadingCoeff (X + ↑C r) ^ i = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
r : R
i : ℕ
✝ : Nontrivial R
⊢ leadingCoeff (X + ↑C r) ^ i ≠ 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Ring R
n : ℕ
hn : 0 < n
r : R
⊢ leadingCoeff (X ^ n - ↑C r) = 1
[PROOFSTEP]
rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_pow_add_C hn]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝¹ : Ring R
inst✝ : Nontrivial R
a : R
⊢ degree (X - ↑C a) = 1
[PROOFSTEP]
rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]
[GOAL]
R : Type u
S : Type v
a b c✝ d : R
n m : ℕ
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : Ring S
c : S
⊢ nextCoeff (X - ↑C c) = -c
[PROOFSTEP]
rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ degree (X ^ n - ↑C a) = ↑n
[PROOFSTEP]
rw [sub_eq_add_neg, ← map_neg C a, degree_X_pow_add_C hn]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n - ↑C a ≠ 0
[PROOFSTEP]
rw [sub_eq_add_neg, ← map_neg C a]
[GOAL]
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + ↑C (-a) ≠ 0
[PROOFSTEP]
exact X_pow_add_C_ne_zero hn _
[GOAL]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ natDegree (X ^ n - ↑C r) = n
[PROOFSTEP]
rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : Ring S
r : S
⊢ leadingCoeff (X - ↑C r) = 1
[PROOFSTEP]
rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp0 : p = 0
⊢ degree (p * q) = degree p + degree q
[PROOFSTEP]
simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp0 : ¬p = 0
hq0 : q = 0
⊢ degree (p * q) = degree p + degree q
[PROOFSTEP]
simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : p = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
[PROOFSTEP]
simp only [hp, zero_mul, leadingCoeff_zero]
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
[PROOFSTEP]
simp only [hq, mul_zero, leadingCoeff_zero]
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
[PROOFSTEP]
rw [leadingCoeff_mul']
[GOAL]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
[PROOFSTEP]
exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)
[GOAL]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ leadingCoeff 1 = 1
[PROOFSTEP]
simp


[GOAL]
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
⊢ p ^ (k + l + 1) ∣ natAbs m * natAbs n
[PROOFSTEP]
rw [← Int.natAbs_mul]
[GOAL]
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
⊢ p ^ (k + l + 1) ∣ natAbs (m * n)
[PROOFSTEP]
apply Int.coe_nat_dvd.1 <| Int.dvd_natAbs.2 hpmn
[GOAL]
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd1 : p ^ (k + 1) ∣ natAbs m
⊢ ↑(p ^ (k + 1)) ∣ m
[PROOFSTEP]
apply Int.dvd_natAbs.1
[GOAL]
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd1 : p ^ (k + 1) ∣ natAbs m
⊢ ↑(p ^ (k + 1)) ∣ ↑(natAbs m)
[PROOFSTEP]
apply Int.coe_nat_dvd.2 hsd1
[GOAL]
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd2 : p ^ (l + 1) ∣ natAbs n
⊢ ↑(p ^ (l + 1)) ∣ n
[PROOFSTEP]
apply Int.dvd_natAbs.1
[GOAL]
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd2 : p ^ (l + 1) ∣ natAbs n
⊢ ↑(p ^ (l + 1)) ∣ ↑(natAbs n)
[PROOFSTEP]
apply Int.coe_nat_dvd.2 hsd2
[GOAL]
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ natAbs k
[PROOFSTEP]
apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp
[GOAL]
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ natAbs k ^ 2
[PROOFSTEP]
rwa [sq, ← natAbs_mul, ← coe_nat_dvd_left, ← sq]