Theorem: MvPolynomial.support_sum_monomial_subset' (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
S : Finset α
g : α → ι →₀ ℕ
f : α → R
⊢ (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
Tactic:
letI := Classical.decEq α
State after:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
S : Finset α
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
⊢ (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S

State before:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
S : Finset α
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
⊢ (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
Tactic:
induction' S using Finset.induction with s S hs hsi
State after:
case empty
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
⊢ (∑ v ∈ ∅, (monomial (g v)) (f v)).support ⊆ image g ∅

case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ (∑ v ∈ insert s S, (monomial (g v)) (f v)).support ⊆ image g (insert s S)

State before:
case empty
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
⊢ (∑ v ∈ ∅, (monomial (g v)) (f v)).support ⊆ image g ∅
Tactic:
simp
State after:
no goals

State before:
case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ (∑ v ∈ insert s S, (monomial (g v)) (f v)).support ⊆ image g (insert s S)
Tactic:
rw [Finset.sum_insert hs]
State after:
case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ ((monomial (g s)) (f s) + ∑ x ∈ S, (monomial (g x)) (f x)).support ⊆ image g (insert s S)

State before:
case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ ((monomial (g s)) (f s) + ∑ x ∈ S, (monomial (g x)) (f x)).support ⊆ image g (insert s S)
Tactic:
apply Finset.Subset.trans support_add
State after:
case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ ((monomial (g s)) (f s)).support ∪ (∑ x ∈ S, (monomial (g x)) (f x)).support ⊆ image g (insert s S)

State before:
case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ ((monomial (g s)) (f s)).support ∪ (∑ x ∈ S, (monomial (g x)) (f x)).support ⊆ image g (insert s S)
Tactic:
apply Finset.union_subset
State after:
case insert.hs
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ ((monomial (g s)) (f s)).support ⊆ image g (insert s S)

case insert.a
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ (∑ x ∈ S, (monomial (g x)) (f x)).support ⊆ image g (insert s S)

State before:
case insert.hs
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ ((monomial (g s)) (f s)).support ⊆ image g (insert s S)
Tactic:
apply Finset.Subset.trans support_monomial_subset _
State after:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ {g s} ⊆ image g (insert s S)

State before:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ {g s} ⊆ image g (insert s S)
Tactic:
rw [Finset.image_insert]
State after:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ {g s} ⊆ insert (g s) (image g S)

State before:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ {g s} ⊆ insert (g s) (image g S)
Tactic:
exact union_subset_left fun ⦃a⦄ a => a
State after:
no goals

State before:
case insert.a
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ (∑ x ∈ S, (monomial (g x)) (f x)).support ⊆ image g (insert s S)
Tactic:
apply Finset.Subset.trans hsi _
State after:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ image g S ⊆ image g (insert s S)

State before:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ image g S ⊆ image g (insert s S)
Tactic:
rw [Finset.image_insert]
State after:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ image g S ⊆ insert (g s) (image g S)

State before:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ image g S ⊆ insert (g s) (image g S)
Tactic:
exact Finset.subset_insert (g s) (Finset.image g S)
State after:
no goals