internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.homogenization_monomial
Proof state before:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ homogenization i ((monomial s) r) = (monomial s) r
Tactic:
erw [homogenization, Finsupp.mapDomain_single, single_eq_monomial, totalDegree_monomial _ hr,
  tsub_self]
Proof state after:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ (monomial (s + Finsupp.single i 0)) r = (monomial s) r
Theorem: MvPolynomial.homogenization_monomial
Proof state before:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ (monomial (s + Finsupp.single i 0)) r = (monomial s) r
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_monomial
Proof state before:
case pos
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : r = 0
⊢ homogenization i ((monomial s) r) = (monomial s) r
Tactic:
simp [hr]
Proof state after:
no goals
Theorem: MvPolynomial.aux
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree
Tactic:
classical
rw [Finsupp.sum_add_index]
rw [Finsupp.sum_single_index]
rw [add_tsub_cancel_iff_le]
apply Finset.le_sup hp
rfl
intros
rfl
intros
rfl
Proof state after:
no goals
Theorem: MvPolynomial.aux
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree
Tactic:
rw [Finsupp.sum_add_index]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x.sum fun x m => m) + (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Theorem: MvPolynomial.aux
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x.sum fun x m => m) + (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
rw [Finsupp.sum_single_index]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ (x.sum fun x m => m) + (p.totalDegree - x.sum fun x m => m) = p.totalDegree

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Theorem: MvPolynomial.aux
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ (x.sum fun x m => m) + (p.totalDegree - x.sum fun x m => m) = p.totalDegree

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
rw [add_tsub_cancel_iff_le]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ (x.sum fun x m => m) ≤ p.totalDegree

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Theorem: MvPolynomial.aux
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ (x.sum fun x m => m) ≤ p.totalDegree

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
apply Finset.le_sup hp
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Theorem: MvPolynomial.aux
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
rfl
Proof state after:
case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Theorem: MvPolynomial.aux
Proof state before:
case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
intros
Proof state after:
case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
a✝¹ : ι
a✝ : a✝¹ ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support
⊢ 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Theorem: MvPolynomial.aux
Proof state before:
case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
a✝¹ : ι
a✝ : a✝¹ ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support
⊢ 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
rfl
Proof state after:
case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Theorem: MvPolynomial.aux
Proof state before:
case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
intros
Proof state after:
case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
a✝¹ : ι
a✝ : a✝¹ ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support
b₁✝ b₂✝ : ℕ
⊢ b₁✝ + b₂✝ = b₁✝ + b₂✝
Theorem: MvPolynomial.aux
Proof state before:
case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
a✝¹ : ι
a✝ : a✝¹ ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support
b₁✝ b₂✝ : ℕ
⊢ b₁✝ + b₂✝ = b₁✝ + b₂✝
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (homogenization i p).IsHomogeneous p.totalDegree
Tactic:
letI := Classical.decEq ι
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ (homogenization i p).IsHomogeneous p.totalDegree
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ (homogenization i p).IsHomogeneous p.totalDegree
Tactic:
rw [homogenization]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ IsHomogeneous (Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p) p.totalDegree
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ IsHomogeneous (Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p) p.totalDegree
Tactic:
intro d hd
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : coeff d (Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : coeff d (Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Tactic:
rw [Finsupp.mapDomain, Finsupp.sum, coeff_sum] at hd
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : ∑ x ∈ p.support, coeff d (Finsupp.single (x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)) (p x)) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : ∑ x ∈ p.support, coeff d (Finsupp.single (x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)) (p x)) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Tactic:
simp_rw [single_eq_monomial, coeff_monomial] at hd
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Tactic:
contrapose! hd
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0
Tactic:
have : ∀ (x : ι →₀ ℕ) (_ : x ∈ p.support),
    ¬x + Finsupp.single i (p.totalDegree - x.sum fun (_x : ι) (m : ℕ) => m) = d := by
  intro x hx hh
  apply hd
  rw [← hh, weightedDegree_one]
  change ((x + Finsupp.single i (p.totalDegree - x.sum fun _ m => m)).sum fun _ m => m) = _
  rw [aux hx]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0
Tactic:
rw [← Finset.sum_coe_sort]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ i_1 : { x // x ∈ p.support },
      if ↑i_1 + Finsupp.single i (p.totalDegree - (↑i_1).sum fun x m => m) = d then p ↑i_1 else 0) =
    0
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ i_1 : { x // x ∈ p.support },
      if ↑i_1 + Finsupp.single i (p.totalDegree - (↑i_1).sum fun x m => m) = d then p ↑i_1 else 0) =
    0
Tactic:
conv_lhs =>
  congr; rfl; ext i
  rw [if_neg (this i.1 i.2)]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ ∑ i : { x // x ∈ p.support }, 0 = 0
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ ∑ i : { x // x ∈ p.support }, 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
⊢ ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
Tactic:
intro x hx hh
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ False
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ False
Tactic:
apply hd
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (weightedDegree 1) d = p.totalDegree
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (weightedDegree 1) d = p.totalDegree
Tactic:
rw [← hh, weightedDegree_one]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ degree (x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m)) = p.totalDegree
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ degree (x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m)) = p.totalDegree
Tactic:
change ((x + Finsupp.single i (p.totalDegree - x.sum fun _ m => m)).sum fun _ m => m) = _
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree
Theorem: MvPolynomial.isHomogeneous_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree
Tactic:
rw [aux hx]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
⊢ homogenization i p = p
Tactic:
by_cases hpn : p = 0
Proof state after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : p = 0
⊢ homogenization i p = p

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ homogenization i p = p
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ homogenization i p = p
Tactic:
rw [homogenization]
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
have := (hp.totalDegree hpn).symm
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
this : n = p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
this : n = p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
subst this
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : p.IsHomogeneous p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : p.IsHomogeneous p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
rw [IsHomogeneous] at hp
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p