Theorem: MvPolynomial.support_prod (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
P : Finset (MvPolynomial ι R)
⊢ (P.prod id).support ⊆ P.sum support
Tactic:
induction' P using Finset.induction with p S hS hSi
State after:
case empty
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
⊢ (∅.prod id).support ⊆ ∅.sum support

case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ ((insert p S).prod id).support ⊆ (insert p S).sum support

State before:
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ ((insert p S).prod id).support ⊆ (insert p S).sum support
Tactic:
rw [Finset.prod_insert hS, Finset.sum_insert hS]
State after:
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ (id p * ∏ x ∈ S, id x).support ⊆ p.support + ∑ x ∈ S, x.support

State before:
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ (id p * ∏ x ∈ S, id x).support ⊆ p.support + ∑ x ∈ S, x.support
Tactic:
simp only [id]
State after:
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ (p * ∏ x ∈ S, x).support ⊆ p.support + ∑ x ∈ S, x.support

State before:
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ (p * ∏ x ∈ S, x).support ⊆ p.support + ∑ x ∈ S, x.support
Tactic:
refine' Finset.Subset.trans (support_mul' _ _) _
State after:
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ p.support + (∏ x ∈ S, x).support ⊆ p.support + ∑ x ∈ S, x.support

State before:
case insert
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p : MvPolynomial ι R
S : Finset (MvPolynomial ι R)
hS : p ∉ S
hSi : (S.prod id).support ⊆ S.sum support
⊢ p.support + (∏ x ∈ S, x).support ⊆ p.support + ∑ x ∈ S, x.support
Tactic:
convert Finset.add_subset_add (Finset.Subset.refl _) hSi
State after:
no goals

State before:
case empty
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
⊢ (∅.prod id).support ⊆ ∅.sum support
Tactic:
simp only [prod_empty, sum_empty]
State after:
case empty
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
⊢ support 1 ⊆ 0

State before:
case empty
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
⊢ support 1 ⊆ 0
Tactic:
exact support_one
State after:
no goals