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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ v, (v.sum fun x e => e) = p.totalDegree ∧ coeff v p ≠ 0
Tactic:
obtain ⟨b, hb₁, hb₂⟩ :=
  p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : ι →₀ ℕ =>
    Multiset.card (Finsupp.toMultiset m)
State after:
case intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ ∃ v, (v.sum fun x e => e) = p.totalDegree ∧ coeff v p ≠ 0

State before:
case intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ ∃ v, (v.sum fun x e => e) = p.totalDegree ∧ coeff v p ≠ 0
Tactic:
use b
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ (b.sum fun x e => e) = p.totalDegree ∧ coeff b p ≠ 0

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ (b.sum fun x e => e) = p.totalDegree ∧ coeff b p ≠ 0
Tactic:
constructor
State after:
case h.left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ (b.sum fun x e => e) = p.totalDegree

case h.right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ coeff b p ≠ 0

State before:
case h.left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ (b.sum fun x e => e) = p.totalDegree
Tactic:
rw [← totalDegree_eq p] at hb₂
State after:
case h.left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : p.totalDegree = Multiset.card (Finsupp.toMultiset b)
⊢ (b.sum fun x e => e) = p.totalDegree

State before:
case h.left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : p.totalDegree = Multiset.card (Finsupp.toMultiset b)
⊢ (b.sum fun x e => e) = p.totalDegree
Tactic:
rw [hb₂]
State after:
case h.left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : p.totalDegree = Multiset.card (Finsupp.toMultiset b)
⊢ (b.sum fun x e => e) = Multiset.card (Finsupp.toMultiset b)

State before:
case h.left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : p.totalDegree = Multiset.card (Finsupp.toMultiset b)
⊢ (b.sum fun x e => e) = Multiset.card (Finsupp.toMultiset b)
Tactic:
exact (Finsupp.card_toMultiset _).symm
State after:
no goals

State before:
case h.right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ coeff b p ≠ 0
Tactic:
exact mem_support_iff.mp hb₁
State after:
no goals