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

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

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

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

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

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

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

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

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

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

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

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