internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof 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
Proof 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)
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof 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
Proof 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)
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof 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 _
Proof 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)
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof 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]
Proof 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)
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof 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 _
Proof 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)
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof 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]
Proof 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)
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof 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)
Proof state after:
no goals
Theorem: MvPolynomial.support_mul'
Proof state before:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (p * q).support ⊆ p.support + q.support
Tactic:
rw [p.as_sum, q.as_sum, Finset.sum_mul_sum, ← Finset.sum_product']
Proof state after:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (∑ x ∈ p.support ×ˢ q.support, (monomial x.1) (coeff x.1 p) * (monomial x.2) (coeff x.2 q)).support ⊆
    (∑ v ∈ p.support, (monomial v) (coeff v p)).support + (∑ v ∈ q.support, (monomial v) (coeff v q)).support
Theorem: MvPolynomial.support_mul'
Proof state before:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (∑ x ∈ p.support ×ˢ q.support, (monomial x.1) (coeff x.1 p) * (monomial x.2) (coeff x.2 q)).support ⊆
    (∑ v ∈ p.support, (monomial v) (coeff v p)).support + (∑ v ∈ q.support, (monomial v) (coeff v q)).support
Tactic:
simp_rw [monomial_mul]
Proof state after:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (∑ x ∈ p.support ×ˢ q.support, (monomial (x.1 + x.2)) (coeff x.1 p * coeff x.2 q)).support ⊆
    (∑ v ∈ p.support, (monomial v) (coeff v p)).support + (∑ v ∈ q.support, (monomial v) (coeff v q)).support
Theorem: MvPolynomial.support_mul'
Proof state before:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (∑ x ∈ p.support ×ˢ q.support, (monomial (x.1 + x.2)) (coeff x.1 p * coeff x.2 q)).support ⊆
    (∑ v ∈ p.support, (monomial v) (coeff v p)).support + (∑ v ∈ q.support, (monomial v) (coeff v q)).support
Tactic:
rw [support_sum_monomial_coeff, support_sum_monomial_coeff]
Proof state after:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (∑ x ∈ p.support ×ˢ q.support, (monomial (x.1 + x.2)) (coeff x.1 p * coeff x.2 q)).support ⊆ p.support + q.support
Theorem: MvPolynomial.support_mul'
Proof state before:
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
p q : MvPolynomial ι R
⊢ (∑ x ∈ p.support ×ˢ q.support, (monomial (x.1 + x.2)) (coeff x.1 p * coeff x.2 q)).support ⊆ p.support + q.support
Tactic:
convert Finset.Subset.trans (support_sum_monomial_subset' _ _ _) (Finset.Subset.refl _)
Proof state after:
no goals
Theorem: MvPolynomial.support_prod
Proof 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
Proof 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
Theorem: MvPolynomial.support_prod
Proof 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]
Proof 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
Theorem: MvPolynomial.support_prod
Proof 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]
Proof 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
Theorem: MvPolynomial.support_prod
Proof 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' _ _) _
Proof 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
Theorem: MvPolynomial.support_prod
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.support_prod
Proof 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]
Proof state after:
case empty
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
⊢ support 1 ⊆ 0
Theorem: MvPolynomial.support_prod
Proof state before:
case empty
R : Type u_2
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
⊢ support 1 ⊆ 0
Tactic:
exact support_one
Proof state after:
no goals
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ degreeOf i p = 0 ↔ ∀ j ∈ p.support, j i = 0
Tactic:
rw [degreeOf_eq_sup]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (p.support.sup fun m => m i) = 0 ↔ ∀ j ∈ p.support, j i = 0
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (p.support.sup fun m => m i) = 0 ↔ ∀ j ∈ p.support, j i = 0
Tactic:
apply Iff.intro
Proof state after:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (p.support.sup fun m => m i) = 0 → ∀ j ∈ p.support, j i = 0

case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (∀ j ∈ p.support, j i = 0) → (p.support.sup fun m => m i) = 0
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (p.support.sup fun m => m i) = 0 → ∀ j ∈ p.support, j i = 0
Tactic:
intro h j hj
Proof state after:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : (p.support.sup fun m => m i) = 0
j : ι →₀ ℕ
hj : j ∈ p.support
⊢ j i = 0
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : (p.support.sup fun m => m i) = 0
j : ι →₀ ℕ
hj : j ∈ p.support
⊢ j i = 0
Tactic:
apply Nat.eq_zero_of_le_zero
Proof state after:
case mp.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : (p.support.sup fun m => m i) = 0
j : ι →₀ ℕ
hj : j ∈ p.support
⊢ j i ≤ 0
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mp.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : (p.support.sup fun m => m i) = 0
j : ι →₀ ℕ
hj : j ∈ p.support
⊢ j i ≤ 0
Tactic:
rw [← h]
Proof state after:
case mp.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : (p.support.sup fun m => m i) = 0
j : ι →₀ ℕ
hj : j ∈ p.support
⊢ j i ≤ p.support.sup fun m => m i
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mp.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : (p.support.sup fun m => m i) = 0
j : ι →₀ ℕ
hj : j ∈ p.support
⊢ j i ≤ p.support.sup fun m => m i
Tactic:
apply Finset.le_sup hj
Proof state after:
no goals
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (∀ j ∈ p.support, j i = 0) → (p.support.sup fun m => m i) = 0
Tactic:
intro h
Proof state after:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ (p.support.sup fun m => m i) = 0
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ (p.support.sup fun m => m i) = 0
Tactic:
apply Nat.eq_zero_of_le_zero
Proof state after:
case mpr.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ (p.support.sup fun m => m i) ≤ 0
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mpr.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ (p.support.sup fun m => m i) ≤ 0
Tactic:
apply Finset.sup_le
Proof state after:
case mpr.h.a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ ∀ b ∈ p.support, b i ≤ 0
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mpr.h.a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ ∀ b ∈ p.support, b i ≤ 0
Tactic:
intro m hm
Proof state after:
case mpr.h.a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
m : ι →₀ ℕ
hm : m ∈ p.support
⊢ m i ≤ 0
Theorem: MvPolynomial.degreeOf_eq_zero_iff
Proof state before:
case mpr.h.a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
m : ι →₀ ℕ
hm : m ∈ p.support
⊢ m i ≤ 0
Tactic:
rw [h m hm]
Proof state after:
no goals
Theorem: MvPolynomial.prod_contains_no
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
hp : ∀ p ∈ P, ∀ j ∈ p.support, j i = 0
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ j i = 0
Tactic:
apply (degreeOf_eq_zero_iff i (P.prod id)).1 _ j hjp
Proof state after:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
hp : ∀ p ∈ P, ∀ j ∈ p.support, j i = 0
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ degreeOf i (P.prod id) = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
hp : ∀ p ∈ P, ∀ j ∈ p.support, j i = 0
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ degreeOf i (P.prod id) = 0
Tactic:
revert hp
Proof state after:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ (∀ p ∈ P, ∀ j ∈ p.support, j i = 0) → degreeOf i (P.prod id) = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ (∀ p ∈ P, ∀ j ∈ p.support, j i = 0) → degreeOf i (P.prod id) = 0
Tactic:
refine' Finset.cons_induction_on P _ _
Proof state after:
case refine'_1
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ (∀ p ∈ ∅, ∀ j ∈ p.support, j i = 0) → degreeOf i (∅.prod id) = 0

case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ ∀ ⦃a : MvPolynomial ι R⦄ {s : Finset (MvPolynomial ι R)} (h : a ∉ s),
    ((∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0) →
      (∀ p ∈ cons a s h, ∀ j ∈ p.support, j i = 0) → degreeOf i ((cons a s h).prod id) = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_1
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ (∀ p ∈ ∅, ∀ j ∈ p.support, j i = 0) → degreeOf i (∅.prod id) = 0
Tactic:
intro _
Proof state after:
case refine'_1
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
hp✝ : ∀ p ∈ ∅, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (∅.prod id) = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_1
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
hp✝ : ∀ p ∈ ∅, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (∅.prod id) = 0
Tactic:
simp only [prod_empty, ← C_1, degreeOf_C]
Proof state after:
no goals
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ ∀ ⦃a : MvPolynomial ι R⦄ {s : Finset (MvPolynomial ι R)} (h : a ∉ s),
    ((∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0) →
      (∀ p ∈ cons a s h, ∀ j ∈ p.support, j i = 0) → degreeOf i ((cons a s h).prod id) = 0
Tactic:
intro a s has hs
Proof state after:
case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
⊢ (∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0) → degreeOf i ((cons a s has).prod id) = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
⊢ (∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0) → degreeOf i ((cons a s has).prod id) = 0
Tactic:
intro hp
Proof state after:
case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i ((cons a s has).prod id) = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i ((cons a s has).prod id) = 0
Tactic:
rw [prod_cons]
Proof state after:
case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a * ∏ x ∈ s, id x) = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a * ∏ x ∈ s, id x) = 0
Tactic:
apply Nat.eq_zero_of_le_zero
Proof state after:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a * ∏ x ∈ s, id x) ≤ 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a * ∏ x ∈ s, id x) ≤ 0
Tactic:
apply le_trans (degreeOf_mul_le _ _ _)
Proof state after:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a) + degreeOf i (∏ x ∈ s, id x) ≤ 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a) + degreeOf i (∏ x ∈ s, id x) ≤ 0
Tactic:
rw [hs]
Proof state after:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a) + 0 ≤ 0

case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ ∀ p ∈ s, ∀ j ∈ p.support, j i = 0