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

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
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

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
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

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 _ _
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

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 _
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

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]
State after:
no goals

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
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

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
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

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]
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

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
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

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 _ _ _)
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

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]
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

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) + 0 ≤ 0
Tactic:
simp only [id, add_zero, le_zero_iff]
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 a = 0

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 a = 0
Tactic:
exact (degreeOf_eq_zero_iff _ _).2 (hp a (mem_cons_self _ _))
State after:
no goals

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
⊢ ∀ p ∈ s, ∀ j ∈ p.support, j i = 0
Tactic:
intro p hps m hmp
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
p : MvPolynomial ι R
hps : p ∈ s
m : ι →₀ ℕ
hmp : m ∈ p.support
⊢ m i = 0

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
p : MvPolynomial ι R
hps : p ∈ s
m : ι →₀ ℕ
hmp : m ∈ p.support
⊢ m i = 0
Tactic:
apply hp p _ m hmp
State after:
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 : MvPolynomial ι R
hps : p ∈ s
m : ι →₀ ℕ
hmp : m ∈ p.support
⊢ p ∈ cons a s has

State before:
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 : MvPolynomial ι R
hps : p ∈ s
m : ι →₀ ℕ
hmp : m ∈ p.support
⊢ p ∈ cons a s has
Tactic:
simp only [hps, mem_cons, or_true_iff]
State after:
no goals