internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.leadingTerms = p
⊢ ∀ ⦃d : ι →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree 1) d = p.totalDegree
Tactic:
contrapose! h
Proof state after:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : ∃ d, coeff d p ≠ 0 ∧ (weightedDegree 1) d ≠ p.totalDegree
⊢ p.leadingTerms ≠ p
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : ∃ d, coeff d p ≠ 0 ∧ (weightedDegree 1) d ≠ p.totalDegree
⊢ p.leadingTerms ≠ p
Tactic:
rcases h with ⟨h_w, h_h₁, h_h₂⟩
Proof state after:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ p.leadingTerms ≠ p
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ p.leadingTerms ≠ p
Tactic:
rw [leadingTerms, Ne, MvPolynomial.ext_iff]
Proof state after:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ¬∀ (m : ι →₀ ℕ), coeff m ((homogeneousComponent p.totalDegree) p) = coeff m p
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ¬∀ (m : ι →₀ ℕ), coeff m ((homogeneousComponent p.totalDegree) p) = coeff m p
Tactic:
push_neg
Proof state after:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ∃ m, coeff m ((homogeneousComponent p.totalDegree) p) ≠ coeff m p
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ∃ m, coeff m ((homogeneousComponent p.totalDegree) p) ≠ coeff m p
Tactic:
use h_w
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Tactic:
classical
rw [weightedDegree_one] at h_h₂
change ¬(h_w.sum fun (_x : ι) (e : ℕ) => e) = p.totalDegree at h_h₂
simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true_iff, Ne,
  not_false_iff, not_forall, ite_eq_left_iff]
convert h_h₂
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Tactic:
rw [weightedDegree_one] at h_h₂
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : degree h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : degree h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Tactic:
change ¬(h_w.sum fun (_x : ι) (e : ℕ) => e) = p.totalDegree at h_h₂
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Tactic:
simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true_iff, Ne,
  not_false_iff, not_forall, ite_eq_left_iff]
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ ¬degree h_w = p.totalDegree
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ ¬degree h_w = p.totalDegree
Tactic:
convert h_h₂
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ p.leadingTerms = p
Tactic:
rw [leadingTerms_apply]
Proof state after:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) = p
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) = p
Tactic:
rw [(_ :
    (p.support.filter fun s : ι →₀ ℕ => ∑ i : ι in s.support, s i = p.totalDegree) =
      p.support)]
Proof state after:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ p.support, (monomial d) (coeff d p) = p

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ filter (fun s => ∑ i ∈ s.support, s i = p.totalDegree) p.support = p.support
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ p.support, (monomial d) (coeff d p) = p
Tactic:
rw [support_sum_monomial_coeff p]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ filter (fun s => ∑ i ∈ s.support, s i = p.totalDegree) p.support = p.support
Tactic:
rw [Finset.filter_eq_self]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∀ x ∈ p.support, ∑ i ∈ x.support, x i = p.totalDegree
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∀ x ∈ p.support, ∑ i ∈ x.support, x i = p.totalDegree
Tactic:
intro s hs
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ ∑ i ∈ s.support, s i = p.totalDegree
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ ∑ i ∈ s.support, s i = p.totalDegree
Tactic:
rw [mem_support_iff] at hs
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : coeff s p ≠ 0
⊢ ∑ i ∈ s.support, s i = p.totalDegree
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : coeff s p ≠ 0
⊢ ∑ i ∈ s.support, s i = p.totalDegree
Tactic:
rw [← h hs, weightedDegree_one]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : coeff s p ≠ 0
⊢ ∑ i ∈ s.support, s i = degree s
Theorem: MvPolynomial.leadingTerms_eq_self_iff_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : coeff s p ≠ 0
⊢ ∑ i ∈ s.support, s i = degree s
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).leadingTerms = C r
Tactic:
rw [leadingTerms_eq_self_iff_isHomogeneous]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).IsHomogeneous (C r).totalDegree
Theorem: MvPolynomial.leadingTerms_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).IsHomogeneous (C r).totalDegree
Tactic:
convert isHomogeneous_C (R := R) _ _
Proof state after:
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).totalDegree = 0
Theorem: MvPolynomial.leadingTerms_C
Proof state before:
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).totalDegree = 0
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
⊢ leadingTerms 0 = 0
Tactic:
simp [leadingTerms]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_one
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
⊢ leadingTerms 1 = 1
Tactic:
simp [leadingTerms]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_monomial
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
⊢ ((monomial s) r).leadingTerms = (monomial s) r
Tactic:
by_cases hr : r = 0
Proof state after:
case pos
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r

case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r
Theorem: MvPolynomial.leadingTerms_monomial
Proof state before:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r
Tactic:
rw [leadingTerms_eq_self_iff_isHomogeneous]
Proof state after:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).IsHomogeneous ((monomial s) r).totalDegree
Theorem: MvPolynomial.leadingTerms_monomial
Proof state before:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).IsHomogeneous ((monomial s) r).totalDegree
Tactic:
convert isHomogeneous_monomial (R := R) _ _
Proof state after:
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = ((monomial s) r).totalDegree
Theorem: MvPolynomial.leadingTerms_monomial
Proof state before:
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = ((monomial s) r).totalDegree
Tactic:
simp [totalDegree_monomial _ hr]
Proof state after:
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = s.sum fun x e => e
Theorem: MvPolynomial.leadingTerms_monomial
Proof state before:
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = s.sum fun x e => e
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_monomial
Proof state before:
case pos
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r
Tactic:
simp [hr]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_X
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
⊢ (X s).leadingTerms = X s
Tactic:
nontriviality R
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).leadingTerms = X s
Theorem: MvPolynomial.leadingTerms_X
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).leadingTerms = X s
Tactic:
rw [leadingTerms_eq_self_iff_isHomogeneous]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).IsHomogeneous (X s).totalDegree
Theorem: MvPolynomial.leadingTerms_X
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).IsHomogeneous (X s).totalDegree
Tactic:
convert isHomogeneous_X _ _
Proof state after:
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).totalDegree = 1
Theorem: MvPolynomial.leadingTerms_X
Proof state before:
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).totalDegree = 1
Tactic:
exact totalDegree_X _
Proof state after:
no goals
Theorem: MvPolynomial.exists_coeff_ne_zero_totalDegree
Proof 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)
Proof 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
Theorem: MvPolynomial.exists_coeff_ne_zero_totalDegree
Proof 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
Proof 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
Theorem: MvPolynomial.exists_coeff_ne_zero_totalDegree
Proof 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
Proof 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
Theorem: MvPolynomial.exists_coeff_ne_zero_totalDegree
Proof 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₂
Proof 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
Theorem: MvPolynomial.exists_coeff_ne_zero_totalDegree
Proof 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₂]
Proof 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)
Theorem: MvPolynomial.exists_coeff_ne_zero_totalDegree
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.exists_coeff_ne_zero_totalDegree
Proof 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₁
Proof state after:
no goals
Theorem: MvPolynomial.add_ne_zero_of_ne_zero_of_support_disjoint
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
hp : p ≠ 0
h : Disjoint p.support q.support
⊢ p + q ≠ 0
Tactic:
classical
contrapose! hp
have := congr_arg support hp
rw [support_zero, support_add_eq h,
  Finset.union_eq_empty,MvPolynomial.support_eq_empty] at this
exact this.left
Proof state after:
no goals
Theorem: MvPolynomial.add_ne_zero_of_ne_zero_of_support_disjoint
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
hp : p ≠ 0
h : Disjoint p.support q.support
⊢ p + q ≠ 0
Tactic:
contrapose! hp
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
⊢ p = 0
Theorem: MvPolynomial.add_ne_zero_of_ne_zero_of_support_disjoint
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
⊢ p = 0
Tactic:
have := congr_arg support hp
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : (p + q).support = support 0
⊢ p = 0
Theorem: MvPolynomial.add_ne_zero_of_ne_zero_of_support_disjoint
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : (p + q).support = support 0
⊢ p = 0
Tactic:
rw [support_zero, support_add_eq h,
  Finset.union_eq_empty,MvPolynomial.support_eq_empty] at this
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : p = 0 ∧ q.support = ∅
⊢ p = 0
Theorem: MvPolynomial.add_ne_zero_of_ne_zero_of_support_disjoint
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : p = 0 ∧ q.support = ∅
⊢ p = 0
Tactic:
exact this.left
Proof state after:
no goals
Theorem: MvPolynomial.support_sum_monomial_eq
Proof state before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
Tactic:
letI := Classical.decEq ι
Proof state after:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
Theorem: MvPolynomial.support_sum_monomial_eq
Proof state before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
Tactic:
induction' S using Finset.induction with s S hs hsi
Proof state after:
case empty
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ ∅, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) ∅

case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ (∑ v ∈ insert s S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) (insert s S)
Theorem: MvPolynomial.support_sum_monomial_eq
Proof state before:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ (∑ v ∈ insert s S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) (insert s S)
Tactic:
rw [Finset.sum_insert hs, support_add_eq]
Proof state after:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ ((monomial s) (f s)).support ∪ (∑ x ∈ S, (monomial x) (f x)).support = filter (fun v => f v ≠ 0) (insert s S)

case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ Disjoint ((monomial s) (f s)).support (∑ x ∈ S, (monomial x) (f x)).support
Theorem: MvPolynomial.support_sum_monomial_eq
Proof state before:
case empty
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ ∅, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) ∅
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.support_sum_monomial_eq
Proof state before:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ ((monomial s) (f s)).support ∪ (∑ x ∈ S, (monomial x) (f x)).support = filter (fun v => f v ≠ 0) (insert s S)
Tactic:
rw [hsi, filter_insert, support_monomial]
Proof state after:
case insert
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
⊢ (if f s = 0 then ∅ else {s}) ∪ filter (fun v => f v ≠ 0) S =
    if f s ≠ 0 then insert s (filter (fun v => f v ≠ 0) S) else filter (fun v => f v ≠ 0) S