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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
⊢ ∃ p_rest, p = p.leadingTerms + p_rest ∧ p_rest.totalDegree < p.totalDegree
Tactic:
letI := Classical.decEq ι
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ∃ p_rest, p = p.leadingTerms + p_rest ∧ p_rest.totalDegree < p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ∃ p_rest, p = p.leadingTerms + p_rest ∧ p_rest.totalDegree < p.totalDegree
Tactic:
exists ∑ v : ι →₀ ℕ in p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = p.leadingTerms + ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p) ∧
    (∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)).totalDegree < p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = p.leadingTerms + ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p) ∧
    (∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)).totalDegree < p.totalDegree
Tactic:
constructor
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = p.leadingTerms + ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)).totalDegree < p.totalDegree

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = p.leadingTerms + ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
nth_rw 1 [p.leadingTerms.as_sum]
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p =
    ∑ v ∈ p.leadingTerms.support, (monomial v) (coeff v p.leadingTerms) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p =
    ∑ v ∈ p.leadingTerms.support, (monomial v) (coeff v p.leadingTerms) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
have : ∀ (x : ι →₀ ℕ) (_ : x ∈ p.leadingTerms.support), x.support.sum x = p.totalDegree :=
  by
  intro x hx
  rw [support_leadingTerms] at hx
  simp at hx
  exact hx.2
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ v ∈ p.leadingTerms.support, (monomial v) (coeff v p.leadingTerms) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ v ∈ p.leadingTerms.support, (monomial v) (coeff v p.leadingTerms) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
simp_rw [coeff_leadingTerms]
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ x ∈ p.leadingTerms.support, (monomial x) (if ∑ i ∈ x.support, x i = p.totalDegree then coeff x p else 0) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ x ∈ p.leadingTerms.support, (monomial x) (if ∑ i ∈ x.support, x i = p.totalDegree then coeff x p else 0) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
rw [← Finset.sum_coe_sort (support (leadingTerms p))]
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ i : { x // x ∈ p.leadingTerms.support },
        (monomial ↑i) (if ∑ i_1 ∈ (↑i).support, ↑i i_1 = p.totalDegree then coeff (↑i) p else 0) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ i : { x // x ∈ p.leadingTerms.support },
        (monomial ↑i) (if ∑ i_1 ∈ (↑i).support, ↑i i_1 = p.totalDegree then coeff (↑i) p else 0) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
conv_rhs =>
  congr; congr; rfl; ext i;
  rw [this i.1 i.2]
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ i : { x // x ∈ p.leadingTerms.support },
        (monomial ↑i) (if p.totalDegree = p.totalDegree then coeff (↑i) p else 0) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ i : { x // x ∈ p.leadingTerms.support },
        (monomial ↑i) (if p.totalDegree = p.totalDegree then coeff (↑i) p else 0) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
simp only [ite_true]
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ x : { x // x ∈ p.leadingTerms.support }, (monomial ↑x) (coeff (↑x) p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ x : { x // x ∈ p.leadingTerms.support }, (monomial ↑x) (coeff (↑x) p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
rw [Finset.sum_coe_sort _ (fun x => (monomial x) (coeff x p))]
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ i ∈ p.leadingTerms.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ i ∈ p.leadingTerms.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
have : p.leadingTerms.support ⊆ p.support := support_leadingTerms_subset _
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝¹ : DecidableEq ι := Classical.decEq ι
this✝ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this : p.leadingTerms.support ⊆ p.support
⊢ p =
    ∑ i ∈ p.leadingTerms.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝¹ : DecidableEq ι := Classical.decEq ι
this✝ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this : p.leadingTerms.support ⊆ p.support
⊢ p =
    ∑ i ∈ p.leadingTerms.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
have : p.leadingTerms.support ∩ p.support = p.leadingTerms.support := by
  rw [Finset.inter_eq_left]
  exact this
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝² : DecidableEq ι := Classical.decEq ι
this✝¹ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this✝ : p.leadingTerms.support ⊆ p.support
this : p.leadingTerms.support ∩ p.support = p.leadingTerms.support
⊢ p =
    ∑ i ∈ p.leadingTerms.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝² : DecidableEq ι := Classical.decEq ι
this✝¹ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this✝ : p.leadingTerms.support ⊆ p.support
this : p.leadingTerms.support ∩ p.support = p.leadingTerms.support
⊢ p =
    ∑ i ∈ p.leadingTerms.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
nth_rw 1 [← this]
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝² : DecidableEq ι := Classical.decEq ι
this✝¹ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this✝ : p.leadingTerms.support ⊆ p.support
this : p.leadingTerms.support ∩ p.support = p.leadingTerms.support
⊢ p =
    ∑ i ∈ p.leadingTerms.support ∩ p.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝² : DecidableEq ι := Classical.decEq ι
this✝¹ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this✝ : p.leadingTerms.support ⊆ p.support
this : p.leadingTerms.support ∩ p.support = p.leadingTerms.support
⊢ p =
    ∑ i ∈ p.leadingTerms.support ∩ p.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
rw [Finset.inter_comm, Finset.sum_inter_add_sum_diff]
State after:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝² : DecidableEq ι := Classical.decEq ι
this✝¹ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this✝ : p.leadingTerms.support ⊆ p.support
this : p.leadingTerms.support ∩ p.support = p.leadingTerms.support
⊢ p = ∑ x ∈ p.support, (monomial x) (coeff x p)

State before:
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝² : DecidableEq ι := Classical.decEq ι
this✝¹ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this✝ : p.leadingTerms.support ⊆ p.support
this : p.leadingTerms.support ∩ p.support = p.leadingTerms.support
⊢ p = ∑ x ∈ p.support, (monomial x) (coeff x p)
Tactic:
exact p.as_sum
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
Tactic:
intro x hx
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
x : ι →₀ ℕ
hx : x ∈ p.leadingTerms.support
⊢ x.support.sum ⇑x = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
x : ι →₀ ℕ
hx : x ∈ p.leadingTerms.support
⊢ x.support.sum ⇑x = p.totalDegree
Tactic:
rw [support_leadingTerms] at hx
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
x : ι →₀ ℕ
hx : x ∈ filter (fun d => (d.sum fun x m => m) = p.totalDegree) p.support
⊢ x.support.sum ⇑x = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
x : ι →₀ ℕ
hx : x ∈ filter (fun d => (d.sum fun x m => m) = p.totalDegree) p.support
⊢ x.support.sum ⇑x = p.totalDegree
Tactic:
simp at hx
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
x : ι →₀ ℕ
hx : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = p.totalDegree
⊢ x.support.sum ⇑x = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
x : ι →₀ ℕ
hx : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = p.totalDegree
⊢ x.support.sum ⇑x = p.totalDegree
Tactic:
exact hx.2
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝¹ : DecidableEq ι := Classical.decEq ι
this✝ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this : p.leadingTerms.support ⊆ p.support
⊢ p.leadingTerms.support ∩ p.support = p.leadingTerms.support
Tactic:
rw [Finset.inter_eq_left]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝¹ : DecidableEq ι := Classical.decEq ι
this✝ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this : p.leadingTerms.support ⊆ p.support
⊢ p.leadingTerms.support ⊆ p.support

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝¹ : DecidableEq ι := Classical.decEq ι
this✝ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this : p.leadingTerms.support ⊆ p.support
⊢ p.leadingTerms.support ⊆ p.support
Tactic:
exact this
State after:
no goals

State before:
case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)).totalDegree < p.totalDegree
Tactic:
rw [totalDegree, Finset.sup_lt_iff]
State after:
case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ 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

State before:
case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ 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
Tactic:
intro b hb
State after:
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

State before:
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
Tactic:
rw [support_leadingTerms] at hb
State after:
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

State before:
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
Tactic:
rw [← Finset.filter_not] at hb
State after:
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 ∈ filter (fun a => ¬(a.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

State before:
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 ∈ filter (fun a => ¬(a.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
Tactic:
have := support_sum_monomial_subset _ _ hb
State after:
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this : b ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) 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

State before:
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this : b ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) 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
Tactic:
simp only [Finset.mem_filter] at this
State after:
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this : b ∈ p.support ∧ ¬(b.sum fun x m => m) = p.totalDegree
⊢ (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

State before:
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this : b ∈ p.support ∧ ¬(b.sum fun x m => m) = p.totalDegree
⊢ (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
Tactic:
cases' this with this_left this_right
State after:
case right.intro
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this_left : b ∈ p.support
this_right : ¬(b.sum fun x m => m) = p.totalDegree
⊢ (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

State before:
case right.intro
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this_left : b ∈ p.support
this_right : ¬(b.sum fun x m => m) = p.totalDegree
⊢ (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
Tactic:
rw [totalDegree]
State after:
case right.intro
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this_left : b ∈ p.support
this_right : ¬(b.sum fun x m => m) = p.totalDegree
⊢ (b.sum fun x e => e) < p.support.sup fun s => s.sum fun x e => e

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

State before:
case right.intro
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this_left : b ∈ p.support
this_right : ¬(b.sum fun x m => m) = p.totalDegree
⊢ (b.sum fun x e => e) < p.support.sup fun s => s.sum fun x e => e

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
Tactic:
refine' lt_of_le_of_ne (by apply Finset.le_sup this_left) this_right
State after:
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

State before:
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
Tactic:
rw [bot_eq_zero]
State after:
case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ 0 < p.totalDegree

State before:
case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ 0 < p.totalDegree
Tactic:
exact pos_iff_ne_zero.mpr hp
State after:
no goals

State before:
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 ∈ filter (fun a => ¬(a.sum fun x m => m) = p.totalDegree) p.support, (monomial v) (coeff v p)).support
this_left : b ∈ p.support
this_right : ¬(b.sum fun x m => m) = p.totalDegree
⊢ (b.sum fun x e => e) ≤ p.support.sup fun s => s.sum fun x e => e
Tactic:
apply Finset.le_sup this_left
State after:
no goals