internlm/Lean-Github huggingface dataset:
Theorem: toSupported_isHomogeneous'
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : ¬0 < nm.1
⊢ IsWeightedHomogeneous Prod.fst (↑1) nm.1
Tactic:
simp only [not_lt, le_zero_iff] at h
Proof state after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : nm.1 = 0
⊢ IsWeightedHomogeneous Prod.fst (↑1) nm.1
Theorem: toSupported_isHomogeneous'
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : nm.1 = 0
⊢ IsWeightedHomogeneous Prod.fst (↑1) nm.1
Tactic:
rw [h, OneMemClass.coe_one]
Proof state after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : nm.1 = 0
⊢ IsWeightedHomogeneous Prod.fst 1 0
Theorem: toSupported_isHomogeneous'
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : nm.1 = 0
⊢ IsWeightedHomogeneous Prod.fst 1 0
Tactic:
apply isWeightedHomogeneous_one
Proof state after:
no goals
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : (weightedDegree Prod.fst) d = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Tactic:
rw [weightedDegree_apply, Finsupp.sum] at hd
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Tactic:
have hnm : ∃ nm : ℕ × M, d nm • nm.fst = 1 := by
  by_contra h0
  rw [not_exists] at h0
  have hd0 : (d.support.sum fun a : ℕ × M => d a • a.fst) = 0 := by
    rw [Finset.sum_eq_zero]
    intro nm hnm
    rw [← Nat.lt_one_iff]
    apply lt_of_le_of_ne _ (h0 nm)
    rw [← hd]
    exact Finset.single_le_sum (fun x _ => zero_le (d x • x.fst)) hnm
  rw [hd0] at hd
  exact zero_ne_one hd
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
hnm : ∃ nm, d nm • nm.1 = 1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
hnm : ∃ nm, d nm • nm.1 = 1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Tactic:
obtain ⟨nm, hnm⟩ := hnm
Proof state after:
case intro
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hnm : d nm • nm.1 = 1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case intro
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hnm : d nm • nm.1 = 1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Tactic:
rw [← hnm] at hd
Proof state after:
case intro
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm • nm.1 = 1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case intro
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm • nm.1 = 1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Tactic:
simp only [Algebra.id.smul_eq_mul, mul_eq_one] at hnm
Proof state after:
case intro
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case intro
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
⊢ ∃ m, Finsupp.single (1, m) 1 = d
Tactic:
use nm.snd
Proof state after:
case h
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
⊢ Finsupp.single (1, nm.2) 1 = d
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case h
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
⊢ Finsupp.single (1, nm.2) 1 = d
Tactic:
ext ab
Proof state after:
case h.h
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
⊢ (Finsupp.single (1, nm.2) 1) ab = d ab
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case h.h
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
⊢ (Finsupp.single (1, nm.2) 1) ab = d ab
Tactic:
rw [Finsupp.single_apply]
Proof state after:
case h.h
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
⊢ (if (1, nm.2) = ab then 1 else 0) = d ab
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case h.h
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
⊢ (if (1, nm.2) = ab then 1 else 0) = d ab
Tactic:
split_ifs with hab <;> rw [← hnm.2, eq_comm, Prod.mk.eta] at hab
Proof state after:
case pos
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ab = nm
⊢ 1 = d ab

case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
⊢ 0 = d ab
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
⊢ ∃ nm, d nm • nm.1 = 1
Tactic:
by_contra h0
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ¬∃ nm, d nm • nm.1 = 1
⊢ False
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ¬∃ nm, d nm • nm.1 = 1
⊢ False
Tactic:
rw [not_exists] at h0
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
⊢ False
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
⊢ False
Tactic:
have hd0 : (d.support.sum fun a : ℕ × M => d a • a.fst) = 0 := by
  rw [Finset.sum_eq_zero]
  intro nm hnm
  rw [← Nat.lt_one_iff]
  apply lt_of_le_of_ne _ (h0 nm)
  rw [← hd]
  exact Finset.single_le_sum (fun x _ => zero_le (d x • x.fst)) hnm
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
hd0 : ∑ a ∈ d.support, d a • a.1 = 0
⊢ False
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
hd0 : ∑ a ∈ d.support, d a • a.1 = 0
⊢ False
Tactic:
rw [hd0] at hd
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : 0 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
hd0 : ∑ a ∈ d.support, d a • a.1 = 0
⊢ False
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : 0 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
hd0 : ∑ a ∈ d.support, d a • a.1 = 0
⊢ False
Tactic:
exact zero_ne_one hd
Proof state after:
no goals
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
⊢ ∑ a ∈ d.support, d a • a.1 = 0
Tactic:
rw [Finset.sum_eq_zero]
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
⊢ ∀ x ∈ d.support, d x • x.1 = 0
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
⊢ ∀ x ∈ d.support, d x • x.1 = 0
Tactic:
intro nm hnm
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
nm : ℕ × M
hnm : nm ∈ d.support
⊢ d nm • nm.1 = 0
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
nm : ℕ × M
hnm : nm ∈ d.support
⊢ d nm • nm.1 = 0
Tactic:
rw [← Nat.lt_one_iff]
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
nm : ℕ × M
hnm : nm ∈ d.support
⊢ d nm • nm.1 < 1
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
nm : ℕ × M
hnm : nm ∈ d.support
⊢ d nm • nm.1 < 1
Tactic:
apply lt_of_le_of_ne _ (h0 nm)
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
nm : ℕ × M
hnm : nm ∈ d.support
⊢ d nm • nm.1 ≤ 1
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
nm : ℕ × M
hnm : nm ∈ d.support
⊢ d nm • nm.1 ≤ 1
Tactic:
rw [← hd]
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
nm : ℕ × M
hnm : nm ∈ d.support
⊢ d nm • nm.1 ≤ ∑ a ∈ d.support, d a • a.1
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hd : ∑ a ∈ d.support, d a • a.1 = 1
hsupp : ∀ nm ∈ d.support, 0 < nm.1
h0 : ∀ (x : ℕ × M), ¬d x • x.1 = 1
nm : ℕ × M
hnm : nm ∈ d.support
⊢ d nm • nm.1 ≤ ∑ a ∈ d.support, d a • a.1
Tactic:
exact Finset.single_le_sum (fun x _ => zero_le (d x • x.fst)) hnm
Proof state after:
no goals
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case pos
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ab = nm
⊢ 1 = d ab
Tactic:
rw [hab, hnm.1]
Proof state after:
no goals
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
⊢ 0 = d ab
Tactic:
rw [eq_comm]
Proof state after:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
⊢ d ab = 0
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
⊢ d ab = 0
Tactic:
by_contra hab'
Proof state after:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
⊢ False
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
⊢ False
Tactic:
have hne0 : d ab * ab.fst ≠ 0 :=
  mul_ne_zero hab' (ne_of_gt (hsupp ab (Finsupp.mem_support_iff.mpr hab')))
Proof state after:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
⊢ False
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
⊢ False
Tactic:
have hnm_mem : nm ∈ d.support := by rw [Finsupp.mem_support_iff, hnm.1]; exact one_ne_zero
Proof state after:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
hnm_mem : nm ∈ d.support
⊢ False
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
hnm_mem : nm ∈ d.support
⊢ False
Tactic:
simp only [Finset.sum_eq_sum_diff_singleton_add hnm_mem, add_left_eq_self,
  Algebra.id.smul_eq_mul, sum_eq_zero_iff, mem_sdiff,
  Finsupp.mem_support_iff, mem_singleton] at hd
Proof state after:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
hnm_mem : nm ∈ d.support
hd : ∀ (x : ℕ × M), d x ≠ 0 ∧ ¬x = nm → d x * x.1 = 0
⊢ False
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
case neg
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
hnm_mem : nm ∈ d.support
hd : ∀ (x : ℕ × M), d x ≠ 0 ∧ ¬x = nm → d x * x.1 = 0
⊢ False
Tactic:
exact hne0 (hd ab ⟨hab', hab⟩)
Proof state after:
no goals
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
⊢ nm ∈ d.support
Tactic:
rw [Finsupp.mem_support_iff, hnm.1]
Proof state after:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
⊢ 1 ≠ 0
Theorem: eq_finsupp_single_of_degree_one
Proof state before:
R : Type ?u.209305
M : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq M
d : ℕ × M →₀ ℕ
hsupp : ∀ nm ∈ d.support, 0 < nm.1
nm : ℕ × M
hd : ∑ a ∈ d.support, d a • a.1 = d nm • nm.1
hnm : d nm = 1 ∧ nm.1 = 1
ab : ℕ × M
hab : ¬ab = nm
hab' : ¬d ab = 0
hne0 : d ab * ab.1 ≠ 0
⊢ 1 ≠ 0
Tactic:
exact one_ne_zero
Proof state after:
no goals
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
⊢ (weightedHomogeneousComponent w m) p = p
Tactic:
ext x
Proof state after:
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m) p) = coeff x p
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same
Proof state before:
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m) p) = coeff x p
Tactic:
rw [coeff_weightedHomogeneousComponent]
Proof state after:
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same
Proof state before:
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p
Tactic:
by_cases zero_coeff : coeff x p = 0
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p
Tactic:
split_ifs
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : (weightedDegree w) x = m
⊢ coeff x p = coeff x p

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = m
⊢ 0 = coeff x p