no goals
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.166872
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ vars (∏ i in s, f i) ⊆ Finset.biUnion s fun i => vars (f i)
classical
induction s using Finset.induction_on with
| empty => simp
| insert hs hsub =>
  simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset_union (Finset.Subset.refl _) hsub
no goals
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.166872
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ vars (∏ i in s, f i) ⊆ Finset.biUnion s fun i => vars (f i)
induction s using Finset.induction_on with
| empty => simp
| insert hs hsub =>
  simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset_union (Finset.Subset.refl _) hsub
no goals
case empty
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.166872
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
⊢ vars (∏ i in ∅, f i) ⊆ Finset.biUnion ∅ fun i => vars (f i)
simp
case insert
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.166872
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (f a✝ * ∏ i in s✝, f i) ⊆ vars (f a✝) ∪ Finset.biUnion s✝ fun i => vars (f i)
case insert
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.166872
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (∏ i in insert a✝ s✝, f i) ⊆ Finset.biUnion (insert a✝ s✝) fun i => vars (f i)
simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
case insert
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.166872
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (f a✝) ∪ vars (∏ i in s✝, f i) ⊆ vars (f a✝) ∪ Finset.biUnion s✝ fun i => vars (f i)
case insert
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.166872
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (f a✝ * ∏ i in s✝, f i) ⊆ vars (f a✝) ∪ Finset.biUnion s✝ fun i => vars (f i)
apply Finset.Subset.trans (vars_mul _ _)
no goals
case insert
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.166872
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : ¬a✝ ∈ s✝
hsub : vars (∏ i in s✝, f i) ⊆ Finset.biUnion s✝ fun i => vars (f i)
⊢ vars (f a✝) ∪ vars (∏ i in s✝, f i) ⊆ vars (f a✝) ∪ Finset.biUnion s✝ fun i => vars (f i)
exact Finset.union_subset_union (Finset.Subset.refl _) hsub