internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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)
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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]
Proof 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)
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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]
Proof 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)
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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]
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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]
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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]
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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]
Proof 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
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.eq_leadingTerms_add
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_add_of_totalDegree_lt
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : q.totalDegree < p.totalDegree
⊢ (p + q).leadingTerms = p.leadingTerms
Tactic:
rw [leadingTerms, leadingTerms, totalDegree_add_eq_left_of_totalDegree_lt h,
  LinearMap.map_add, homogeneousComponent_eq_zero _ q h, add_zero]
Proof state after:
no goals
Theorem: MvPolynomial.NoZeroSmulDivisors.smul_eq_zero_iff_eq_zero_or_eq_zero
Proof state before:
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0
Tactic:
constructor <;> intro h
Proof state after:
case mp
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c • x = 0
⊢ c = 0 ∨ x = 0

case mpr
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c = 0 ∨ x = 0
⊢ c • x = 0
Theorem: MvPolynomial.NoZeroSmulDivisors.smul_eq_zero_iff_eq_zero_or_eq_zero
Proof state before:
case mp
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c • x = 0
⊢ c = 0 ∨ x = 0

case mpr
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c = 0 ∨ x = 0
⊢ c • x = 0
Tactic:
exact eq_zero_or_eq_zero_of_smul_eq_zero h
Proof state after:
case mpr
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c = 0 ∨ x = 0
⊢ c • x = 0
Theorem: MvPolynomial.NoZeroSmulDivisors.smul_eq_zero_iff_eq_zero_or_eq_zero
Proof state before:
case mpr
R✝ : Type ?u.165782
ι : Type ?u.165785
inst✝⁴ : CommSemiring R✝
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
h : c = 0 ∨ x = 0
⊢ c • x = 0
Tactic:
cases' h with h h <;> simp [h]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_C_mul
Proof state before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Tactic:
by_cases hr : r = 0
Proof state after:
case pos
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms

case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Theorem: MvPolynomial.leadingTerms_C_mul
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Tactic:
have : support (C r * p) = p.support := by
  rw [C_mul']
  exact Finsupp.support_smul_eq hr
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Theorem: MvPolynomial.leadingTerms_C_mul
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Tactic:
rw [leadingTerms, leadingTerms, totalDegree, this, homogeneousComponent_C_mul]
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ C r * (homogeneousComponent (p.support.sup fun s => s.sum fun x e => e)) p =
    C r * (homogeneousComponent p.totalDegree) p
Theorem: MvPolynomial.leadingTerms_C_mul
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ C r * (homogeneousComponent (p.support.sup fun s => s.sum fun x e => e)) p =
    C r * (homogeneousComponent p.totalDegree) p
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_C_mul
Proof state before:
case pos
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Tactic:
simp [hr]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_C_mul
Proof state before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (C r * p).support = p.support
Tactic:
rw [C_mul']
Proof state after:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (r • p).support = p.support
Theorem: MvPolynomial.leadingTerms_C_mul
Proof state before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (r • p).support = p.support
Tactic:
exact Finsupp.support_smul_eq hr
Proof state after:
no goals
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree = 0
⊢ p = C (coeff 0 p)
Tactic:
letI := Classical.decEq ι
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree = 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree = 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)
Tactic:
erw [Finset.sup_eq_bot_iff] at hp
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ∀ s ∈ p.support, (s.sum fun x e => e) = ⊥
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)