Theorem: PolynomialMap.Finsupp.sum_eq_one_iff (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (d.sum fun x n => n) = 1 ↔ ∃ a, Finsupp.single a 1 = d
Tactic:
constructor
State after:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (d.sum fun x n => n) = 1 → ∃ a, Finsupp.single a 1 = d

case mpr
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (∃ a, Finsupp.single a 1 = d) → (d.sum fun x n => n) = 1

State before:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (d.sum fun x n => n) = 1 → ∃ a, Finsupp.single a 1 = d
Tactic:
intro h1
State after:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
⊢ ∃ a, Finsupp.single a 1 = d

State before:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
have hd0 : d ≠ 0 := by
  intro h
  simp only [h, Finsupp.sum_zero_index, zero_ne_one] at h1
State after:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
⊢ ∃ a, Finsupp.single a 1 = d

State before:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
obtain ⟨a, ha⟩ := Finsupp.ne_iff.mp hd0
State after:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
⊢ ∃ a, Finsupp.single a 1 = d

State before:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
rw [Finsupp.coe_zero, Pi.zero_apply, ne_eq] at ha
State after:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ ∃ a, Finsupp.single a 1 = d

State before:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
rw [← Finsupp.add_sum_erase' _ a, Nat.add_eq_one_iff] at h1
State after:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : d a = 0 ∧ ((Finsupp.erase a d).sum fun x n => n) = 1 ∨ d a = 1 ∧ ((Finsupp.erase a d).sum fun x n => n) = 0
ha : ¬d a = 0
⊢ ∃ a, Finsupp.single a 1 = d

case mp.intro.hg
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ α → 0 = 0

State before:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : d a = 0 ∧ ((Finsupp.erase a d).sum fun x n => n) = 1 ∨ d a = 1 ∧ ((Finsupp.erase a d).sum fun x n => n) = 0
ha : ¬d a = 0
⊢ ∃ a, Finsupp.single a 1 = d

case mp.intro.hg
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ α → 0 = 0
Tactic:
rcases h1 with (⟨ha', _⟩ | ⟨ha, ha'⟩)
State after:
case mp.intro.inl.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
ha' : d a = 0
right✝ : ((Finsupp.erase a d).sum fun x n => n) = 1
⊢ ∃ a, Finsupp.single a 1 = d

case mp.intro.inr.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ((Finsupp.erase a d).sum fun x n => n) = 0
⊢ ∃ a, Finsupp.single a 1 = d

case mp.intro.hg
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ α → 0 = 0

State before:
case mp.intro.hg
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ α → 0 = 0
Tactic:
exact fun _ ↦ rfl
State after:
no goals

State before:
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
⊢ d ≠ 0
Tactic:
intro h
State after:
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
h : d = 0
⊢ False

State before:
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
h : d = 0
⊢ False
Tactic:
simp only [h, Finsupp.sum_zero_index, zero_ne_one] at h1
State after:
no goals

State before:
case mp.intro.inl.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
ha' : d a = 0
right✝ : ((Finsupp.erase a d).sum fun x n => n) = 1
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
exfalso
State after:
case mp.intro.inl.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
ha' : d a = 0
right✝ : ((Finsupp.erase a d).sum fun x n => n) = 1
⊢ False

State before:
case mp.intro.inl.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
ha' : d a = 0
right✝ : ((Finsupp.erase a d).sum fun x n => n) = 1
⊢ False
Tactic:
exact ha ha'
State after:
no goals

State before:
case mp.intro.inr.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ((Finsupp.erase a d).sum fun x n => n) = 0
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
use a
State after:
case h
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ((Finsupp.erase a d).sum fun x n => n) = 0
⊢ Finsupp.single a 1 = d

State before:
case h
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ((Finsupp.erase a d).sum fun x n => n) = 0
⊢ Finsupp.single a 1 = d
Tactic:
simp only [Finsupp.sum, Finsupp.support_erase, sum_eq_zero_iff, mem_erase] at ha'
State after:
case h
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
⊢ Finsupp.single a 1 = d

State before:
case h
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
⊢ Finsupp.single a 1 = d
Tactic:
ext b
State after:
case h.h
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
⊢ (Finsupp.single a 1) b = d b

State before:
case h.h
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
⊢ (Finsupp.single a 1) b = d b
Tactic:
by_cases hb : a = b
State after:
case pos
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : a = b
⊢ (Finsupp.single a 1) b = d b

case neg
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ (Finsupp.single a 1) b = d b

State before:
case pos
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : a = b
⊢ (Finsupp.single a 1) b = d b
Tactic:
rw [← hb, Finsupp.single_eq_same, ha]
State after:
no goals

State before:
case neg
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ (Finsupp.single a 1) b = d b
Tactic:
rw [Finsupp.single_eq_of_ne hb]
State after:
case neg
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ 0 = d b

State before:
case neg
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ 0 = d b
Tactic:
apply symm
State after:
case neg.a
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ d b = 0

State before:
case neg.a
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ d b = 0
Tactic:
simp only [ne_eq, Finsupp.mem_support_iff, and_imp] at ha'
State after:
case neg.a
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
b : α
hb : ¬a = b
ha' : ∀ (x : α), ¬x = a → ¬d x = 0 → (Finsupp.erase a d) x = 0
⊢ d b = 0

State before:
case neg.a
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
b : α
hb : ¬a = b
ha' : ∀ (x : α), ¬x = a → ¬d x = 0 → (Finsupp.erase a d) x = 0
⊢ d b = 0
Tactic:
simpa only [Finsupp.erase_ne (ne_comm.mp hb), _root_.not_imp_self] using ha' b (ne_comm.mp hb)
State after:
no goals

State before:
case mpr
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (∃ a, Finsupp.single a 1 = d) → (d.sum fun x n => n) = 1
Tactic:
rintro ⟨a, rfl⟩
State after:
case mpr.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ((Finsupp.single a 1).sum fun x n => n) = 1

State before:
case mpr.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ((Finsupp.single a 1).sum fun x n => n) = 1
Tactic:
rw [Finsupp.sum_eq_single a, Finsupp.single_eq_same]
State after:
case mpr.intro.h₀
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ∀ (b : α), (Finsupp.single a 1) b ≠ 0 → b ≠ a → (Finsupp.single a 1) b = 0

case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0

State before:
case mpr.intro.h₀
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ∀ (b : α), (Finsupp.single a 1) b ≠ 0 → b ≠ a → (Finsupp.single a 1) b = 0

case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
intro b hb hb'
State after:
case mpr.intro.h₀
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ (Finsupp.single a 1) b = 0

case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0

State before:
case mpr.intro.h₀
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ (Finsupp.single a 1) b = 0

case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
exfalso
State after:
case mpr.intro.h₀
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ False

case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0

State before:
case mpr.intro.h₀
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ False

case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
apply hb
State after:
case mpr.intro.h₀
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ (Finsupp.single a 1) b = 0

case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0

State before:
case mpr.intro.h₀
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ (Finsupp.single a 1) b = 0

case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
rw [Finsupp.single_eq_of_ne hb'.symm]
State after:
case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0

State before:
case mpr.intro.h₁
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
exact fun _ ↦ rfl
State after:
no goals