R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.157002
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ vars (p + q)
⊢ x ∈ vars p ∪ vars q
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.157002
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ vars (p + q) ⊆ vars p ∪ vars q
intro x hx
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.157002
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ degrees (p + q)
⊢ x ∈ degrees p ∨ x ∈ degrees q
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.157002
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ vars (p + q)
⊢ x ∈ vars p ∪ vars q
simp only [vars_def, Finset.mem_union, Multiset.mem_toFinset] at hx⊢
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.157002
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ degrees (p + q)
⊢ x ∈ degrees p ∨ x ∈ degrees q
simpa using Multiset.mem_of_le (degrees_add _ _) hx