internlm/Lean-Github huggingface dataset:
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
⊢ (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
Tactic:
split_ifs with h h' <;> simp [h, insert_eq]
Proof state after:
case pos
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
h : f s = 0
h' : f s ≠ 0
⊢ False
Theorem: MvPolynomial.support_sum_monomial_eq
Proof state before:
case pos
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
h : f s = 0
h' : f s ≠ 0
⊢ False
Tactic:
exact h' h
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
⊢ Disjoint ((monomial s) (f s)).support (∑ x ∈ S, (monomial x) (f x)).support
Tactic:
apply disjoint_of_subset_left support_monomial_subset
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
⊢ Disjoint {s} (∑ x ∈ S, (monomial x) (f x)).support
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
⊢ Disjoint {s} (∑ x ∈ S, (monomial x) (f x)).support
Tactic:
simp [hsi, hs]
Proof state after:
no goals
Theorem: MvPolynomial.support_sum_monomial_subset
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ (∑ v ∈ S, (monomial v) (f v)).support ⊆ S
Tactic:
classical
rw [support_sum_monomial_eq]
apply filter_subset
Proof state after:
no goals
Theorem: MvPolynomial.support_sum_monomial_subset
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ (∑ v ∈ S, (monomial v) (f v)).support ⊆ S
Tactic:
rw [support_sum_monomial_eq]
Proof state after:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ filter (fun v => f v ≠ 0) S ⊆ S
Theorem: MvPolynomial.support_sum_monomial_subset
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ filter (fun v => f v ≠ 0) S ⊆ S
Tactic:
apply filter_subset
Proof state after:
no goals
Theorem: MvPolynomial.sum_monomial_ne_zero_of_exists_mem_ne_zero
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
h : ∃ s, ∃ (_ : s ∈ S), f s ≠ 0
⊢ ∑ s ∈ S, (monomial s) (f s) ≠ 0
Tactic:
classical
simp only [← support_eq_empty, support_sum_monomial_eq, Ne]
rcases h with ⟨s, h_S, h_s⟩
exact ne_empty_of_mem (mem_filter.mpr ⟨h_S, h_s⟩)
Proof state after:
no goals
Theorem: MvPolynomial.sum_monomial_ne_zero_of_exists_mem_ne_zero
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
h : ∃ s, ∃ (_ : s ∈ S), f s ≠ 0
⊢ ∑ s ∈ S, (monomial s) (f s) ≠ 0
Tactic:
simp only [← support_eq_empty, support_sum_monomial_eq, Ne]
Proof state after:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
h : ∃ s, ∃ (_ : s ∈ S), f s ≠ 0
⊢ ¬filter (fun v => ¬f v = 0) S = ∅
Theorem: MvPolynomial.sum_monomial_ne_zero_of_exists_mem_ne_zero
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
h : ∃ s, ∃ (_ : s ∈ S), f s ≠ 0
⊢ ¬filter (fun v => ¬f v = 0) S = ∅
Tactic:
rcases h with ⟨s, h_S, h_s⟩
Proof state after:
case intro.intro
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
s : ι →₀ ℕ
h_S : s ∈ S
h_s : f s ≠ 0
⊢ ¬filter (fun v => ¬f v = 0) S = ∅
Theorem: MvPolynomial.sum_monomial_ne_zero_of_exists_mem_ne_zero
Proof state before:
case intro.intro
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
s : ι →₀ ℕ
h_S : s ∈ S
h_s : f s ≠ 0
⊢ ¬filter (fun v => ¬f v = 0) S = ∅
Tactic:
exact ne_empty_of_mem (mem_filter.mpr ⟨h_S, h_s⟩)
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ p.leadingTerms ≠ 0
Tactic:
classical
rw [leadingTerms_apply]
apply sum_monomial_ne_zero_of_exists_mem_ne_zero
simp only [exists_prop, mem_support_iff, Finset.mem_filter]
obtain ⟨f, hf, hf0⟩ := exists_coeff_ne_zero_totalDegree hp
exact ⟨f, ⟨hf0, hf⟩,  hf0⟩
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ p.leadingTerms ≠ 0
Tactic:
rw [leadingTerms_apply]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) ≠ 0
Theorem: MvPolynomial.leadingTerms_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) ≠ 0
Tactic:
apply sum_monomial_ne_zero_of_exists_mem_ne_zero
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, ∃ (_ : s ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support), coeff s p ≠ 0
Theorem: MvPolynomial.leadingTerms_ne_zero
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, ∃ (_ : s ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support), coeff s p ≠ 0
Tactic:
simp only [exists_prop, mem_support_iff, Finset.mem_filter]
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0
Theorem: MvPolynomial.leadingTerms_ne_zero
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0
Tactic:
obtain ⟨f, hf, hf0⟩ := exists_coeff_ne_zero_totalDegree hp
Proof state after:
case h.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
f : ι →₀ ℕ
hf : (f.sum fun x e => e) = p.totalDegree
hf0 : coeff f p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0
Theorem: MvPolynomial.leadingTerms_ne_zero
Proof state before:
case h.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
f : ι →₀ ℕ
hf : (f.sum fun x e => e) = p.totalDegree
hf0 : coeff f p ≠ 0
⊢ ∃ s, (coeff s p ≠ 0 ∧ ∑ i ∈ s.support, s i = p.totalDegree) ∧ coeff s p ≠ 0
Tactic:
exact ⟨f, ⟨hf0, hf⟩,  hf0⟩
Proof state after:
no goals
Theorem: MvPolynomial.totalDegree_leadingTerms
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms.totalDegree = p.totalDegree
Tactic:
by_cases hp : p = 0
Proof state after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p = 0
⊢ p.leadingTerms.totalDegree = p.totalDegree

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ¬p = 0
⊢ p.leadingTerms.totalDegree = p.totalDegree
Theorem: MvPolynomial.totalDegree_leadingTerms
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ¬p = 0
⊢ p.leadingTerms.totalDegree = p.totalDegree
Tactic:
exact totalDegree_homogenous_component_of_ne_zero (leadingTerms_ne_zero hp)
Proof state after:
no goals
Theorem: MvPolynomial.totalDegree_leadingTerms
Proof state before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p = 0
⊢ p.leadingTerms.totalDegree = p.totalDegree
Tactic:
simp [hp]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_idempotent
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms.leadingTerms = p.leadingTerms
Tactic:
rw [leadingTerms_eq_self_iff_isHomogeneous, totalDegree_leadingTerms]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms.IsHomogeneous p.totalDegree
Theorem: MvPolynomial.leadingTerms_idempotent
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms.IsHomogeneous p.totalDegree
Tactic:
exact isHomogeneous_leadingTerms p
Proof state after:
no goals
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ ((homogeneousComponent n) p).support = filter (fun d => (d.sum fun x m => m) = n) p.support
Tactic:
ext x
Proof state after:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ x ∈ ((homogeneousComponent n) p).support ↔ x ∈ filter (fun d => (d.sum fun x m => m) = n) p.support
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ x ∈ ((homogeneousComponent n) p).support ↔ x ∈ filter (fun d => (d.sum fun x m => m) = n) p.support
Tactic:
simp only [mem_support_iff, ne_eq, mem_filter]
Proof state after:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ ¬coeff x ((homogeneousComponent n) p) = 0 ↔ ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ ¬coeff x ((homogeneousComponent n) p) = 0 ↔ ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
Tactic:
refine ⟨fun hx ↦ ⟨fun h ↦ hx <| by simp [coeff_homogeneousComponent, h], ?_⟩,
  fun ⟨h₁, h₂⟩ ↦ fun h ↦ h₁ ?_⟩
Proof state after:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬coeff x ((homogeneousComponent n) p) = 0
⊢ (x.sum fun x m => m) = n

case a.refine_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
x✝ : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
h₁ : ¬coeff x p = 0
h₂ : (x.sum fun x m => m) = n
h : coeff x ((homogeneousComponent n) p) = 0
⊢ coeff x p = 0
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬coeff x ((homogeneousComponent n) p) = 0
h : coeff x p = 0
⊢ coeff x ((homogeneousComponent n) p) = 0
Tactic:
simp [coeff_homogeneousComponent, h]
Proof state after:
no goals
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬coeff x ((homogeneousComponent n) p) = 0
⊢ (x.sum fun x m => m) = n
Tactic:
simp only [coeff_homogeneousComponent, ite_eq_right_iff] at hx
Proof state after:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬(degree x = n → coeff x p = 0)
⊢ (x.sum fun x m => m) = n
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : ¬(degree x = n → coeff x p = 0)
⊢ (x.sum fun x m => m) = n
Tactic:
contrapose! hx
Proof state after:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
⊢ degree x = n → coeff x p = 0
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
⊢ degree x = n → coeff x p = 0
Tactic:
intro h₁
Proof state after:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
h₁ : degree x = n
⊢ coeff x p = 0
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
case a.refine_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
hx : (x.sum fun x m => m) ≠ n
h₁ : degree x = n
⊢ coeff x p = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
case a.refine_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
x✝ : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
h₁ : ¬coeff x p = 0
h₂ : (x.sum fun x m => m) = n
h : coeff x ((homogeneousComponent n) p) = 0
⊢ coeff x p = 0
Tactic:
simp only [coeff_homogeneousComponent, ite_eq_right_iff] at h
Proof state after:
case a.refine_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
x✝ : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
h₁ : ¬coeff x p = 0
h₂ : (x.sum fun x m => m) = n
h : degree x = n → coeff x p = 0
⊢ coeff x p = 0
Theorem: MvPolynomial.support_homogeneousComponent
Proof state before:
case a.refine_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
x✝ : ¬coeff x p = 0 ∧ (x.sum fun x m => m) = n
h₁ : ¬coeff x p = 0
h₂ : (x.sum fun x m => m) = n
h : degree x = n → coeff x p = 0
⊢ coeff x p = 0
Tactic:
exact h h₂
Proof state after:
no goals
Theorem: MvPolynomial.support_homogeneousComponent_subset
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ ((homogeneousComponent n) p).support ⊆ p.support
Tactic:
rw [support_homogeneousComponent]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ filter (fun d => (d.sum fun x m => m) = n) p.support ⊆ p.support
Theorem: MvPolynomial.support_homogeneousComponent_subset
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ filter (fun d => (d.sum fun x m => m) = n) p.support ⊆ p.support
Tactic:
exact Finset.filter_subset _ _
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
⊢ ∃ p_rest, p = p.leadingTerms + p_rest ∧ p_rest.totalDegree < p.totalDegree
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_rest, p = p.leadingTerms + p_rest ∧ p_rest.totalDegree < 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 ι
⊢ ∃ 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)
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 = 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
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 ι
⊢ 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
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 ι
⊢ 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
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 ι
⊢ p = p.leadingTerms + ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
Tactic:
nth_rw 1 [p.leadingTerms.as_sum]
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 ι
⊢ p =
    ∑ v ∈ p.leadingTerms.support, (monomial v) (coeff v p.leadingTerms) +
      ∑ 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 ι
⊢ 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
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
⊢ p =
    ∑ v ∈ p.leadingTerms.support, (monomial v) (coeff v p.leadingTerms) +
      ∑ 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
⊢ 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]
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
⊢ 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)
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
⊢ 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))]
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
⊢ 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)
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
⊢ 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]
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
⊢ 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)
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
⊢ 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]
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
⊢ p =
    ∑ x : { x // x ∈ p.leadingTerms.support }, (monomial ↑x) (coeff (↑x) 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
⊢ 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))]
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
⊢ 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
⊢ 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 _
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
⊢ p =
    ∑ i ∈ p.leadingTerms.support, (monomial i) (coeff i p) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)