no goals
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)
simp only [sum_empty, sup_empty, degree_zero, le_refl]
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))
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))
rw [sum_insert has]
no goals
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))
exact degree_add_le _ _
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))
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)
rw [sup_insert, sup_eq_max]
no goals
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))
exact max_le_max le_rfl ih