case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees (p + q) ≤ degrees p ∪ degrees q

case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ∪ degrees q ≤ degrees (p + q)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees (p + q) = degrees p ∪ degrees q
apply le_antisymm
no goals
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees (p + q) ≤ degrees p ∪ degrees q
apply degrees_add
case a.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ≤ degrees (p + q)

case a.h₂
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees q ≤ degrees (p + q)
case a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ∪ degrees q ≤ degrees (p + q)
apply Multiset.union_le
no goals
case a.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees p ≤ degrees (p + q)
apply le_degrees_add h
case a.h₂
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees q ≤ degrees (q + p)
case a.h₂
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees q ≤ degrees (p + q)
rw [add_comm]
no goals
case a.h₂
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.51214
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
h : Multiset.Disjoint (degrees p) (degrees q)
⊢ degrees q ≤ degrees (q + p)
apply le_degrees_add h.symm