no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.192546
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (∑ i in t, φ i) ⊆ Finset.biUnion t fun i => vars (φ i)
classical
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has]
  refine'
    Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) _)
  assumption
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.192546
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (∑ i in t, φ i) ⊆ Finset.biUnion t fun i => vars (φ i)
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has]
  refine'
    Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) _)
  assumption
no goals
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.192546
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (∑ i in ∅, φ i) ⊆ Finset.biUnion ∅ fun i => vars (φ i)
simp
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.192546
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (φ a✝ + ∑ x in s✝, φ x) ⊆ vars (φ a✝) ∪ Finset.biUnion s✝ fun i => vars (φ i)
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.192546
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ i in insert a✝ s✝, φ i) ⊆ Finset.biUnion (insert a✝ s✝) fun i => vars (φ i)
rw [Finset.biUnion_insert, Finset.sum_insert has]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.192546
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ x in s✝, φ x) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.192546
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (φ a✝ + ∑ x in s✝, φ x) ⊆ vars (φ a✝) ∪ Finset.biUnion s✝ fun i => vars (φ i)
refine'
  Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) _)
no goals
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.192546
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ x in s✝, φ x) ⊆ Finset.biUnion s✝ fun i => vars (φ i)
assumption