R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
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
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
p : R[X]
n : ℕ
a : R
⊢ degree (update p n a) ≤ max (degree p) ↑n
rw [degree, support_update]
case inl
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ Finset.max (Finset.erase (support p) n) ≤ max (degree p) ↑n

case inr
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ Finset.max (insert n (support p)) ≤ max (degree p) ↑n
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
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
split_ifs
no goals
case inl
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ Finset.max (Finset.erase (support p) n) ≤ max (degree p) ↑n
exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
case inr
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ max (Finset.max (support p)) ↑n ≤ max (degree p) ↑n
case inr
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ Finset.max (insert n (support p)) ≤ max (degree p) ↑n
rw [max_insert, max_comm]
no goals
case inr
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.562120
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ max (Finset.max (support p)) ↑n ≤ max (degree p) ↑n
exact le_rfl