internlm/Lean-Github huggingface dataset:
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 : IsWeightedHomogeneous 1 p p.totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
have : ∀ (x) (_ : x ∈ p.support),
    (fun j : ι →₀ ℕ => j + Finsupp.single i (p.totalDegree - j.sum fun (_x : ι) (m : ℕ) => m))
        x = x := by
  intro x hx
  simp only [add_right_eq_self, Finsupp.single_eq_same, tsub_eq_zero_iff_le, Finsupp.single_tsub,
    Finsupp.single_le_iff]
  rw [← hp (mem_support_iff.mp hx), weightedDegree_one]
  exact le_refl _
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
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ 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 : IsWeightedHomogeneous 1 p p.totalDegree
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
Tactic:
rw [Finsupp.mapDomain_congr this]
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
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun x => x) 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 : IsWeightedHomogeneous 1 p p.totalDegree
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun x => x) p = p
Tactic:
erw [Finsupp.mapDomain_id]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
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
Tactic:
simp [hpn]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
⊢ ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
Tactic:
intro x hx
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
Tactic:
simp only [add_right_eq_self, Finsupp.single_eq_same, tsub_eq_zero_iff_le, Finsupp.single_tsub,
  Finsupp.single_le_iff]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ p.totalDegree ≤ x.sum fun _x m => m
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ p.totalDegree ≤ x.sum fun _x m => m
Tactic:
rw [← hp (mem_support_iff.mp hx), weightedDegree_one]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ degree x ≤ x.sum fun _x m => m
Theorem: MvPolynomial.homogenization_of_isHomogeneous
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
⊢ degree x ≤ x.sum fun _x m => m
Tactic:
exact le_refl _
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_idempotent
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ homogenization i (homogenization i p) = homogenization i p
Tactic:
classical
apply homogenization_of_isHomogeneous p.totalDegree
exact isHomogeneous_homogenization _ _
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_idempotent
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ homogenization i (homogenization i p) = homogenization i p
Tactic:
apply homogenization_of_isHomogeneous p.totalDegree
Proof state after:
case hp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (homogenization i p).IsHomogeneous p.totalDegree
Theorem: MvPolynomial.homogenization_idempotent
Proof state before:
case hp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (homogenization i p).IsHomogeneous p.totalDegree
Tactic:
exact isHomogeneous_homogenization _ _
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
⊢ homogenization i p ≠ 0
Tactic:
intro h
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ False
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ False
Tactic:
apply hp
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ p = 0
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ p = 0
Tactic:
refine' Finsupp.mapDomain_injOn _ this _ _ h
Proof state after:
case refine'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ p ∈ {w | ↑w.support ⊆ {w | w i = 0}}

case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ 0 ∈ {w | ↑w.support ⊆ {w | w i = 0}}
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
Tactic:
intro t ht y hy hh
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t ∈ {w | w i = 0}
y : ι →₀ ℕ
hy : y ∈ {w | w i = 0}
hh :
  (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) t =
    (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) y
⊢ t = y
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t ∈ {w | w i = 0}
y : ι →₀ ℕ
hy : y ∈ {w | w i = 0}
hh :
  (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) t =
    (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) y
⊢ t = y
Tactic:
simp only [Set.mem_setOf_eq] at hh hy ht
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
⊢ t = y
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
⊢ t = y
Tactic:
ext a
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
⊢ t a = y a
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
⊢ t a = y a
Tactic:
have :
  (t + Finsupp.single i (p.totalDegree - t.sum fun _ m => m)) a =
    (y + Finsupp.single i (p.totalDegree - y.sum fun _ m => m)) a :=
  by rw [hh]
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  (t + Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    (y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
⊢ t a = y a
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  (t + Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    (y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
⊢ t a = y a
Tactic:
simp only [Finsupp.coe_add, Pi.add_apply] at this
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  t a + (Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    y a + (Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
⊢ t a = y a
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
⊢ (t + Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    (y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
Tactic:
rw [hh]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  t a + (Finsupp.single i (p.totalDegree - t.sum fun x m => m)) a =
    y a + (Finsupp.single i (p.totalDegree - y.sum fun x m => m)) a
⊢ t a = y a
Tactic:
rw [Finsupp.single_apply, Finsupp.single_apply] at this
Proof state after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  (t a + if i = a then p.totalDegree - t.sum fun x m => m else 0) =
    y a + if i = a then p.totalDegree - y.sum fun x m => m else 0
⊢ t a = y a
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
this :
  (t a + if i = a then p.totalDegree - t.sum fun x m => m else 0) =
    y a + if i = a then p.totalDegree - y.sum fun x m => m else 0
⊢ t a = y a
Tactic:
split_ifs at this  with hia
Proof state after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
hia : i = a
this : t a + (p.totalDegree - t.sum fun x m => m) = y a + (p.totalDegree - y.sum fun x m => m)
⊢ t a = y a

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
hia : ¬i = a
this : t a + 0 = y a + 0
⊢ t a = y a
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
hia : i = a
this : t a + (p.totalDegree - t.sum fun x m => m) = y a + (p.totalDegree - y.sum fun x m => m)
⊢ t a = y a
Tactic:
rw [← hia, ht, hy]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
a : ι
hia : ¬i = a
this : t a + 0 = y a + 0
⊢ t a = y a
Tactic:
simpa
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case refine'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ p ∈ {w | ↑w.support ⊆ {w | w i = 0}}
Tactic:
intro x hx
Proof state after:
case refine'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : x ∈ ↑p.support
⊢ x ∈ {w | w i = 0}
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case refine'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : x ∈ ↑p.support
⊢ x ∈ {w | w i = 0}
Tactic:
rw [Set.mem_setOf_eq, hjp x hx]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ 0 ∈ {w | ↑w.support ⊆ {w | w i = 0}}
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ ↑(Finsupp.support 0) ⊆ {w | w i = 0}
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
⊢ ↑(Finsupp.support 0) ⊆ {w | w i = 0}
Tactic:
intro x hx
Proof state after:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : x ∈ ↑(Finsupp.support 0)
⊢ x ∈ {w | w i = 0}
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : x ∈ ↑(Finsupp.support 0)
⊢ x ∈ {w | w i = 0}
Tactic:
simp only [mem_coe, Finsupp.mem_support_iff, ne_eq] at hx
Proof state after:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : ¬0 x = 0
⊢ x ∈ {w | w i = 0}
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : ¬0 x = 0
⊢ x ∈ {w | w i = 0}
Tactic:
change ¬ 0 = 0 at hx
Proof state after:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : ¬0 = 0
⊢ x ∈ {w | w i = 0}
Theorem: MvPolynomial.homogenization_ne_zero_of_ne_zero
Proof state before:
case refine'_2
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
this : Set.InjOn (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) {w | w i = 0}
x : ι →₀ ℕ
hx : ¬0 = 0
⊢ x ∈ {w | w i = 0}
Tactic:
simp only [not_true] at hx
Proof state after:
no goals
Theorem: MvPolynomial.totalDegree_homogenization
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ (homogenization i p).totalDegree = p.totalDegree
Tactic:
by_cases hp : p = 0
Proof state after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree
Theorem: MvPolynomial.totalDegree_homogenization
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree
Tactic:
apply IsHomogeneous.totalDegree
Proof state after:
case neg.hφ
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).IsHomogeneous p.totalDegree

case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ homogenization i p ≠ 0
Theorem: MvPolynomial.totalDegree_homogenization
Proof state before:
case neg.hφ
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).IsHomogeneous p.totalDegree

case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ homogenization i p ≠ 0
Tactic:
refine' isHomogeneous_homogenization _ _
Proof state after:
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ homogenization i p ≠ 0
Theorem: MvPolynomial.totalDegree_homogenization
Proof state before:
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ homogenization i p ≠ 0
Tactic:
exact homogenization_ne_zero_of_ne_zero _ hp h
Proof state after:
no goals
Theorem: MvPolynomial.totalDegree_homogenization
Proof state before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree
Tactic:
simp [hp]
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
⊢ p.leadingTerms = p ↔ p.IsHomogeneous p.totalDegree
Tactic:
constructor <;> intro h
Proof state after:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.leadingTerms = p
⊢ p.IsHomogeneous p.totalDegree

case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous 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 : p.leadingTerms = p
⊢ p.IsHomogeneous p.totalDegree
Tactic:
rw [IsHomogeneous, IsWeightedHomogeneous]
Proof state after:
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