[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : comp p q = 0
⊢ natDegree (comp p q) ≤ natDegree p * natDegree q
[PROOFSTEP]
rw [h0, natDegree_zero]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : comp p q = 0
⊢ 0 ≤ natDegree p * natDegree q
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : ¬comp p q = 0
n : ℕ
hn : n ∈ support p
⊢ ↑(natDegree (↑C (coeff p n))) + n • ↑(natDegree q) = ↑(n * natDegree q)
[PROOFSTEP]
rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : ¬comp p q = 0
n : ℕ
hn : n ∈ support p
⊢ ↑n * ↑(natDegree q) = ↑(n * natDegree q)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : IsRoot p a
hlt : 0 ≥ degree p
⊢ False
[PROOFSTEP]
have := eq_C_of_degree_le_zero hlt
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : IsRoot p a
hlt : 0 ≥ degree p
this : p = ↑C (coeff p 0)
⊢ False
[PROOFSTEP]
rw [IsRoot, this, eval_C] at h 
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : coeff p 0 = 0
hlt : 0 ≥ degree p
this : p = ↑C (coeff p 0)
⊢ False
[PROOFSTEP]
simp only [h, RingHom.map_zero] at this 
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : coeff p 0 = 0
hlt : 0 ≥ degree p
this : p = 0
⊢ False
[PROOFSTEP]
exact hp this
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ natDegree p ≤ n ↔ ∀ (N : ℕ), n < N → coeff p N = 0
[PROOFSTEP]
simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_withBot, WithBot.coe_lt_coe]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
⊢ natDegree (p + q) ≤ n ↔ natDegree p ≤ n
[PROOFSTEP]
refine' ⟨fun h => _, fun h => natDegree_add_le_of_degree_le h qn⟩
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
⊢ natDegree p ≤ n
[PROOFSTEP]
refine' natDegree_le_iff_coeff_eq_zero.mpr fun m hm => _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
m : ℕ
hm : n < m
⊢ coeff p m = 0
[PROOFSTEP]
convert natDegree_le_iff_coeff_eq_zero.mp h m hm using 1
[GOAL]
case h.e'_2
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
m : ℕ
hm : n < m
⊢ coeff p m = coeff (p + q) m
[PROOFSTEP]
rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
pn : natDegree p ≤ n
⊢ natDegree (p + q) ≤ n ↔ natDegree q ≤ n
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
pn : natDegree p ≤ n
⊢ natDegree (q + p) ≤ n ↔ natDegree q ≤ n
[PROOFSTEP]
exact natDegree_add_le_iff_left _ _ pn
[GOAL]
R : Type u
S : Type v
ι : Type w
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
⊢ natDegree (↑C a) + natDegree f = 0 + natDegree f
[PROOFSTEP]
rw [natDegree_C a]
[GOAL]
R : Type u
S : Type v
ι : Type w
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
a : R
⊢ natDegree f + natDegree (↑C a) = natDegree f + 0
[PROOFSTEP]
rw [natDegree_C a]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : ai * a = 1
⊢ natDegree p = natDegree (1 * p)
[PROOFSTEP]
nth_rw 1 [← one_mul p]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : ai * a = 1
⊢ natDegree (1 * p) = natDegree (↑C ai * (↑C a * p))
[PROOFSTEP]
rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : a * ai = 1
⊢ natDegree p = natDegree (p * 1)
[PROOFSTEP]
nth_rw 1 [← mul_one p]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : a * ai = 1
⊢ natDegree (p * 1) = natDegree (p * ↑C a * ↑C ai)
[PROOFSTEP]
rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ natDegree (p * ↑C a) = natDegree p
[PROOFSTEP]
refine' eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ natDegree p ∈ support (p * ↑C a)
[PROOFSTEP]
refine' mem_support_iff.mpr _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ coeff (p * ↑C a) (natDegree p) ≠ 0
[PROOFSTEP]
rwa [coeff_mul_C]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ natDegree (↑C a * p) = natDegree p
[PROOFSTEP]
refine' eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ natDegree p ∈ support (↑C a * p)
[PROOFSTEP]
refine' mem_support_iff.mpr _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ coeff (↑C a * p) (natDegree p) ≠ 0
[PROOFSTEP]
rwa [coeff_C_mul]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f g : R[X]
⊢ coeff (f * g) (natDegree f + natDegree g) = coeff f (natDegree f) * coeff g (natDegree g)
[PROOFSTEP]
simp only [coeff_natDegree, coeff_mul_degree_add_degree]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
[PROOFSTEP]
rcases eq_or_lt_of_le pm with (rfl | hm)
[GOAL]
case inl
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
⊢ coeff (p * q) (natDegree p + n) = coeff p (natDegree p) * coeff q n
[PROOFSTEP]
rcases eq_or_lt_of_le qn with (rfl | hn)
[GOAL]
case inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
[PROOFSTEP]
rcases eq_or_lt_of_le qn with (rfl | hn)
[GOAL]
case inl.inl
R : Type u
S : Type v
ι : Type w
a b : R
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ natDegree p
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (natDegree p + natDegree q) = coeff p (natDegree p) * coeff q (natDegree q)
[PROOFSTEP]
exact natDegree_add_coeff_mul _ _
[GOAL]
case inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
hn : natDegree q < n
⊢ coeff (p * q) (natDegree p + n) = coeff p (natDegree p) * coeff q n
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hn, mul_zero]
[GOAL]
case inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
hn : natDegree q < n
⊢ coeff (p * q) (natDegree p + n) = 0
[PROOFSTEP]
exact natDegree_lt_coeff_mul (add_lt_add_left hn _)
[GOAL]
case inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
hm : natDegree p < m
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (m + natDegree q) = coeff p m * coeff q (natDegree q)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hm, zero_mul]
[GOAL]
case inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
hm : natDegree p < m
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (m + natDegree q) = 0
[PROOFSTEP]
exact natDegree_lt_coeff_mul (add_lt_add_right hm _)
[GOAL]
case inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
hn : natDegree q < n
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hn, mul_zero]
[GOAL]
case inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
hn : natDegree q < n
⊢ coeff (p * q) (m + n) = 0
[PROOFSTEP]
exact natDegree_lt_coeff_mul (add_lt_add hm hn)
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
⊢ coeff (p ^ m) (m * n) = coeff p n ^ m
[PROOFSTEP]
induction' m with m hm
[GOAL]
case zero
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
⊢ coeff (p ^ Nat.zero) (Nat.zero * n) = coeff p n ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (m * n) = coeff p n ^ m
⊢ coeff (p ^ Nat.succ m) (Nat.succ m * n) = coeff p n ^ Nat.succ m
[PROOFSTEP]
rw [pow_succ', pow_succ', ← hm, Nat.succ_mul, coeff_mul_of_natDegree_le _ pn]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (m * n) = coeff p n ^ m
⊢ natDegree (p ^ m) ≤ m * n
[PROOFSTEP]
refine' natDegree_pow_le.trans (le_trans _ (le_refl _))
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (m * n) = coeff p n ^ m
⊢ m * natDegree p ≤ m * n
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left pn m.zero_le
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
o : ℕ
pn : natDegree p ≤ n
mno : m * n ≤ o
⊢ coeff (p ^ m) o = if o = m * n then coeff p n ^ m else 0
[PROOFSTEP]
rcases eq_or_ne o (m * n) with rfl | h
[GOAL]
case inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
mno : m * n ≤ m * n
⊢ coeff (p ^ m) (m * n) = if m * n = m * n then coeff p n ^ m else 0
[PROOFSTEP]
simpa only [ite_true] using coeff_pow_of_natDegree_le pn
[GOAL]
case inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
o : ℕ
pn : natDegree p ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ coeff (p ^ m) o = if o = m * n then coeff p n ^ m else 0
[PROOFSTEP]
simpa only [h, ite_false] using
  coeff_eq_zero_of_natDegree_lt $ lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p < n
⊢ coeff (p + q) n = coeff q n
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p < n
⊢ coeff (q + p) n = coeff q n
[PROOFSTEP]
exact coeff_add_eq_left_of_lt pn
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum s f) = sup s fun i => degree (f i)
[PROOFSTEP]
induction' s using Finset.induction_on with x s hx IH
[GOAL]
case empty
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h✝ : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
h : Set.Pairwise {i | i ∈ ∅ ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum ∅ f) = sup ∅ fun i => degree (f i)
[PROOFSTEP]
simp
[GOAL]
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum (insert x s) f) = sup (insert x s) fun i => degree (f i)
[PROOFSTEP]
simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
[GOAL]
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
specialize IH (h.mono fun _ => by simp (config := { contextual := true }))
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
x✝ : S
⊢ x✝ ∈ {i | i ∈ s ∧ f i ≠ 0} → x✝ ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
[GOAL]
case insert.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) < degree (Finset.sum s f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
[GOAL]
case insert.inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case insert.inr.inl.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h✝ : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
hx : ¬x ∈ ∅
h : Set.Pairwise {i | i ∈ insert x ∅ ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum ∅ f) = sup ∅ fun i => degree (f i)
H : degree (f x) = degree (Finset.sum ∅ f)
⊢ degree (f x + Finset.sum ∅ fun x => f x) = degree (f x) ⊔ sup ∅ fun i => degree (f i)
[PROOFSTEP]
simp
[GOAL]
case insert.inr.inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
hs : Finset.Nonempty s
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
[GOAL]
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
hs : Finset.Nonempty s
y : S
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rw [IH, hy'] at H 
[GOAL]
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
by_cases hx0 : f x = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : f x = 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
simp [hx0, IH]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
have hy0 : f y ≠ 0 := by
  contrapose! H
  simpa [H, degree_eq_bot] using hx0
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
⊢ f y ≠ 0
[PROOFSTEP]
contrapose! H
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
H : f y = 0
⊢ degree (f x) ≠ degree (f y)
[PROOFSTEP]
simpa [H, degree_eq_bot] using hx0
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
refine' absurd H (h _ _ fun H => hx _)
[GOAL]
case neg.refine'_1
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ x ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
[PROOFSTEP]
simp [hx0]
[GOAL]
case neg.refine'_2
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
[PROOFSTEP]
simp [hy, hy0]
[GOAL]
case neg.refine'_3
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H✝ : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s
[PROOFSTEP]
exact H.symm ▸ hy
[GOAL]
case insert.inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (Finset.sum s f) < degree (f x)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
by_cases H : ∃ x ∈ s, f x ≠ 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∃ x, x ∈ s ∧ f x ≠ 0
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
obtain ⟨x, hx, hx'⟩ := H
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
have hs : s.Nonempty := ⟨x, hx⟩
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
refine' natDegree_eq_of_degree_eq_some _
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ degree (Finset.sum s f) = ↑(sup s fun i => natDegree (f i))
[PROOFSTEP]
rw [degree_sum_eq_of_disjoint]
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ (sup s fun i => degree (f i)) = ↑(sup s fun i => natDegree (f i))
[PROOFSTEP]
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, Nat.cast_withBot, Finset.coe_sup' hs, ← Finset.sup'_eq_sup hs]
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ (sup' s hs fun i => degree (f i)) = sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case pos.intro.intro.refine'_1
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ (sup' s hs fun i => degree (f i)) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
rw [Finset.sup'_le_iff]
[GOAL]
case pos.intro.intro.refine'_1
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ ∀ (b : S), b ∈ s → degree (f b) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
intro b hb
[GOAL]
case pos.intro.intro.refine'_1
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
⊢ degree (f b) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
by_cases hb' : f b = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : f b = 0
⊢ degree (f b) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
simpa [hb'] using hs
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ degree (f b) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
rw [degree_eq_natDegree hb', Nat.cast_withBot]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ↑(natDegree (f b)) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb
[GOAL]
case pos.intro.intro.refine'_2
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ sup' s hs (WithBot.some ∘ fun i => natDegree (f i)) ≤ sup' s hs fun i => degree (f i)
[PROOFSTEP]
rw [Finset.sup'_le_iff]
[GOAL]
case pos.intro.intro.refine'_2
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ ∀ (b : S), b ∈ s → (WithBot.some ∘ fun i => natDegree (f i)) b ≤ sup' s hs fun i => degree (f i)
[PROOFSTEP]
intro b hb
[GOAL]
case pos.intro.intro.refine'_2
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
⊢ (WithBot.some ∘ fun i => natDegree (f i)) b ≤ sup' s hs fun i => degree (f i)
[PROOFSTEP]
simp only [Finset.le_sup'_iff, exists_prop, Function.comp_apply]
[GOAL]
case pos.intro.intro.refine'_2
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
⊢ ∃ b_1, b_1 ∈ s ∧ ↑(natDegree (f b)) ≤ degree (f b_1)
[PROOFSTEP]
by_cases hb' : f b = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ∃ b_1, b_1 ∈ s ∧ ↑(natDegree (f b)) ≤ degree (f b_1)
[PROOFSTEP]
refine' ⟨x, hx, _⟩
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ↑(natDegree (f b)) ≤ degree (f x)
[PROOFSTEP]
contrapose! hx'
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : f b = 0
hx' : degree (f x) < ↑(natDegree (f b))
⊢ f x = 0
[PROOFSTEP]
simpa [← Nat.cast_withBot, hb', degree_eq_bot] using hx'
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ∃ b_1, b_1 ∈ s ∧ ↑(natDegree (f b)) ≤ degree (f b_1)
[PROOFSTEP]
exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩
[GOAL]
case pos.intro.intro.h
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
[PROOFSTEP]
exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ¬∃ x, x ∈ s ∧ f x ≠ 0
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
push_neg at H 
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S), x ∈ s → f x = 0
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S), x ∈ s → f x = 0
⊢ ∀ (s_1 : S), s_1 ∈ s → natDegree (f s_1) = ⊥
[PROOFSTEP]
intro x hx
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S), x ∈ s → f x = 0
x : S
hx : x ∈ s
⊢ natDegree (f x) = ⊥
[PROOFSTEP]
simp [H x hx]
[GOAL]
R : Type u
S : Type v
ι : Type w
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q r a : R[X]
⊢ max (natDegree (bit0 a)) (natDegree 1) ≤ natDegree a
[PROOFSTEP]
simp [natDegree_bit0]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
⊢ False
[PROOFSTEP]
have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = ↑C (coeff p 0)
⊢ False
[PROOFSTEP]
rw [A, eval₂_C] at hz 
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : ↑f (coeff p 0) = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = ↑C (coeff p 0)
⊢ False
[PROOFSTEP]
simp only [inj (p.coeff 0) hz, RingHom.map_zero] at A 
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : ↑f (coeff p 0) = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = 0
⊢ False
[PROOFSTEP]
exact hp A
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
⊢ ↑n < degree p ↔ n < natDegree p
[PROOFSTEP]
by_cases h : p = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < degree p ↔ n < natDegree p
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
h : ¬p = 0
⊢ ↑n < degree p ↔ n < natDegree p
[PROOFSTEP]
simp [degree_eq_natDegree h, Nat.cast_withBot, WithBot.coe_lt_coe]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
⊢ natDegree (p - q) = natDegree (q - p)
[PROOFSTEP]
rw [← natDegree_neg, neg_sub]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
qn : natDegree q ≤ n
⊢ natDegree (p - q) ≤ n ↔ natDegree p ≤ n
[PROOFSTEP]
rw [← natDegree_neg] at qn 
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
qn : natDegree (-q) ≤ n
⊢ natDegree (p - q) ≤ n ↔ natDegree p ≤ n
[PROOFSTEP]
rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
pn : natDegree p ≤ n
⊢ natDegree (p - q) ≤ n ↔ natDegree q ≤ n
[PROOFSTEP]
rwa [natDegree_sub, natDegree_sub_le_iff_left]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
dg : natDegree q < n
⊢ coeff (p - q) n = coeff p n
[PROOFSTEP]
rw [← natDegree_neg] at dg 
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
dg : natDegree (-q) < n
⊢ coeff (p - q) n = coeff p n
[PROOFSTEP]
rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
df : natDegree p < n
⊢ coeff (p - q) n = -coeff q n
[PROOFSTEP]
rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
a0 : a ≠ 0
⊢ degree (p * ↑C a) = degree p
[PROOFSTEP]
rw [degree_mul, degree_C a0, add_zero]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
a0 : a ≠ 0
⊢ degree (↑C a * p) = degree p
[PROOFSTEP]
rw [degree_mul, degree_C a0, zero_add]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
a0 : a ≠ 0
⊢ natDegree (p * ↑C a) = natDegree p
[PROOFSTEP]
simp only [natDegree, degree_mul_C a0]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
a0 : a ≠ 0
⊢ natDegree (↑C a * p) = natDegree p
[PROOFSTEP]
simp only [natDegree, degree_C_mul a0]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
by_cases q0 : q.natDegree = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : natDegree q = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C, natDegree_C, mul_zero]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
by_cases p0 : p = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : p = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
simp only [p0, zero_comp, natDegree_zero, zero_mul]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : ¬p = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
refine' le_antisymm natDegree_comp_le (le_natDegree_of_ne_zero _)
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : ¬p = 0
⊢ coeff (comp p q) (natDegree p * natDegree q) ≠ 0
[PROOFSTEP]
simp only [coeff_comp_degree_mul_degree q0, p0, mul_eq_zero, leadingCoeff_eq_zero, or_self_iff,
  ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), pow_ne_zero, Ne.def, not_false_iff]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
k : ℕ
⊢ natDegree ((comp p)^[k] q) = natDegree p ^ k * natDegree q
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ natDegree ((comp p)^[Nat.zero] q) = natDegree p ^ Nat.zero * natDegree q
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
k : ℕ
IH : natDegree ((comp p)^[k] q) = natDegree p ^ k * natDegree q
⊢ natDegree ((comp p)^[Nat.succ k] q) = natDegree p ^ Nat.succ k * natDegree q
[PROOFSTEP]
rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ, mul_assoc]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : natDegree q ≠ 0
⊢ leadingCoeff (comp p q) = leadingCoeff p * leadingCoeff q ^ natDegree p
[PROOFSTEP]
rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]
