Theorem: eq_finsupp_single_of_degree_one (DividedPowers/DPAlgebra/Misc.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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]
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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]
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

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
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

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]
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

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)
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

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]
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

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
State after:
no goals

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]
State after:
no goals

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]
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

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'
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

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')))
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

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
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

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
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

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⟩)
State after:
no goals

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]
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

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
State after:
no goals