rw [support_leadingTerms] at hb
case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
b : ι →₀ ℕ
hb : b ∈ (∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)).support
⊢ (b.sum fun x e => e) < p.totalDegree

case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ⊥ < p.totalDegree
case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
b : ι →₀ ℕ
hb :
  b ∈
    (∑ v ∈ p.support \ filter (fun d => (d.sum fun x m => m) = p.totalDegree) p.support,
        (monomial v) (coeff v p)).support
⊢ (b.sum fun x e => e) < p.totalDegree

case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ⊥ < p.totalDegree