R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (Finset.sup (support (p + q)) fun s => ↑toMultiset s) ≤
    (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ degrees (p + q) ≤ degrees p ⊔ degrees q
simp_rw [degrees_def]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (Finset.sup (support (p + q)) fun s => ↑toMultiset s) ≤
    (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
refine' Finset.sup_le fun b hb => _
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
this : b ∈ p.support ∪ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
have := Finsupp.support_add hb
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
this : b ∈ p.support ∨ b ∈ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
this : b ∈ p.support ∪ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
rw [Finset.mem_union] at this
case inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
h : b ∈ p.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s

case inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
h : b ∈ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
this : b ∈ p.support ∨ b ∈ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
cases' this with h h
no goals
case inl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
h : b ∈ p.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
exact le_sup_of_le_left (Finset.le_sup h)
no goals
case inr
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.31525
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ support (p + q)
h : b ∈ q.support
⊢ ↑toMultiset b ≤ (Finset.sup (support p) fun s => ↑toMultiset s) ⊔ Finset.sup (support q) fun s => ↑toMultiset s
exact le_sup_of_le_right (Finset.le_sup h)