α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
⊢ supported M R s ⊓ ker (lmapDomain M R f) ≤ ⊥
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
⊢ Disjoint (supported M R s) (ker (lmapDomain M R f))
rw [disjoint_iff_inf_le]
case intro
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : l ∈ ↑(ker (lmapDomain M R f))
⊢ l ∈ ⊥
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
⊢ supported M R s ⊓ ker (lmapDomain M R f) ≤ ⊥
rintro l ⟨h₁, h₂⟩
case intro
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
⊢ l ∈ ⊥
case intro
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : l ∈ ↑(ker (lmapDomain M R f))
⊢ l ∈ ⊥
rw [SetLike.mem_coe, mem_ker, lmapDomain_apply, mapDomain] at h₂
case intro
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
⊢ l = 0
case intro
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
⊢ l ∈ ⊥
simp
case intro.h
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
⊢ ↑l x = ↑0 x
case intro
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
⊢ l = 0
ext x
case intro.h
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
⊢ ↑l x = ↑0 x
case intro.h
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
⊢ ↑l x = ↑0 x
haveI := Classical.decPred fun x => x ∈ s
case pos
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : x ∈ s
⊢ ↑l x = ↑0 x

case neg
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : ¬x ∈ s
⊢ ↑l x = ↑0 x
case intro.h
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
⊢ ↑l x = ↑0 x
by_cases xs : x ∈ s
case pos
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ↑(sum l fun a => single (f a)) (f x) = 0
⊢ ↑l x = ↑0 x
case pos
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : x ∈ s
⊢ ↑l x = ↑0 x
have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := by
  rw [h₂]
  rfl
case pos
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ↑l x = 0
⊢ ↑l x = ↑0 x

case pos.h₀
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ∑ a in l.support, ↑(single (f a) (↑l a)) (f x) = 0
⊢ ∀ (b : α), b ∈ l.support → b ≠ x → ↑(single (f b) (↑l b)) (f x) = 0

case pos.h₁
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ∑ a in l.support, ↑(single (f a) (↑l a)) (f x) = 0
⊢ ¬x ∈ l.support → ↑(single (f x) (↑l x)) (f x) = 0
case pos
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ↑(sum l fun a => single (f a)) (f x) = 0
⊢ ↑l x = ↑0 x
rw [Finsupp.sum_apply, Finsupp.sum, Finset.sum_eq_single x, single_eq_same] at this
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : x ∈ s
⊢ ↑0 (f x) = 0
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : x ∈ s
⊢ ↑(sum l fun a => single (f a)) (f x) = 0
rw [h₂]
no goals
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : x ∈ s
⊢ ↑0 (f x) = 0
rfl
no goals
case pos
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ↑l x = 0
⊢ ↑l x = ↑0 x
simpa
case pos.h₀
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ∑ a in l.support, ↑(single (f a) (↑l a)) (f x) = 0
y : α
hy : y ∈ l.support
xy : y ≠ x
⊢ ↑(single (f y) (↑l y)) (f x) = 0
case pos.h₀
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ∑ a in l.support, ↑(single (f a) (↑l a)) (f x) = 0
⊢ ∀ (b : α), b ∈ l.support → b ≠ x → ↑(single (f b) (↑l b)) (f x) = 0
intro y hy xy
no goals
case pos.h₀
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ∑ a in l.support, ↑(single (f a) (↑l a)) (f x) = 0
y : α
hy : y ∈ l.support
xy : y ≠ x
⊢ ↑(single (f y) (↑l y)) (f x) = 0
simp [mt (H _ (h₁ hy) _ xs) xy]
no goals
case pos.h₁
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this✝ : DecidablePred fun x => x ∈ s
xs : x ∈ s
this : ∑ a in l.support, ↑(single (f a) (↑l a)) (f x) = 0
⊢ ¬x ∈ l.support → ↑(single (f x) (↑l x)) (f x) = 0
simp (config := { contextual := true })
case neg
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : ¬x ∈ s
h : ¬↑l x = ↑0 x
⊢ False
case neg
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : ¬x ∈ s
⊢ ↑l x = ↑0 x
by_contra h
no goals
case neg
α : Type u_1
M : Type u_3
N : Type ?u.251779
P : Type ?u.251782
R : Type u_4
S : Type ?u.251788
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_2
α'' : Type ?u.251883
f : α → α'
s : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (sum l fun a => single (f a)) = 0
x : α
this : DecidablePred fun x => x ∈ s
xs : ¬x ∈ s
h : ¬↑l x = ↑0 x
⊢ False
exact xs (h₁ <| Finsupp.mem_support_iff.2 h)