R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint (vars p) (vars q)
⊢ vars p ∪ vars q ⊆ vars (p + q)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint (vars p) (vars q)
⊢ vars (p + q) = vars p ∪ vars q
apply Finset.Subset.antisymm (vars_add_subset p q)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint (vars p) (vars q)
x : σ
hx : x ∈ vars p ∪ vars q
⊢ x ∈ vars (p + q)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint (vars p) (vars q)
⊢ vars p ∪ vars q ⊆ vars (p + q)
intro x hx
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
x : σ
h : Multiset.Disjoint (degrees p) (degrees q)
hx : x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
⊢ x ∈ Multiset.toFinset (degrees (p + q))
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint (vars p) (vars q)
x : σ
hx : x ∈ vars p ∪ vars q
⊢ x ∈ vars (p + q)
simp only [vars_def, Multiset.disjoint_toFinset] at h hx⊢
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
x : σ
h : Multiset.Disjoint (degrees p) (degrees q)
hx : x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
⊢ x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
x : σ
h : Multiset.Disjoint (degrees p) (degrees q)
hx : x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
⊢ x ∈ Multiset.toFinset (degrees (p + q))
rw [degrees_add_of_disjoint h, Multiset.toFinset_union]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.158991
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
x : σ
h : Multiset.Disjoint (degrees p) (degrees q)
hx : x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
⊢ x ∈ Multiset.toFinset (degrees p) ∪ Multiset.toFinset (degrees q)
exact hx