α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ ∑ a_1 in x.support, ↑(single (f a_1) (↑x a_1)) (f a) = ↑x a
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ ↑(mapDomain f x) (f a) = ↑x a
rw [mapDomain, sum_apply, sum]
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ (∑ x_1 in x.support, if f x_1 = f a then ↑x x_1 else 0) = ↑x a
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ ∑ a_1 in x.support, ↑(single (f a_1) (↑x a_1)) (f a) = ↑x a
simp_rw [single_apply]
case pos
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (∑ x_1 in x.support, if f x_1 = f a then ↑x x_1 else 0) = ↑x a

case neg
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : ¬a ∈ x.support
⊢ (∑ x_1 in x.support, if f x_1 = f a then ↑x x_1 else 0) = ↑x a
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ (∑ x_1 in x.support, if f x_1 = f a then ↑x x_1 else 0) = ↑x a
by_cases hax : a ∈ x.support
case pos
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (↑x a + ∑ x_1 in Finset.erase x.support a, if f x_1 = f a then ↑x x_1 else 0) = ↑x a
case pos
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (∑ x_1 in x.support, if f x_1 = f a then ↑x x_1 else 0) = ↑x a
rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
case h.e'_2.h.e'_6
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (∑ x_1 in Finset.erase x.support a, if f x_1 = f a then ↑x x_1 else 0) = 0
case pos
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (↑x a + ∑ x_1 in Finset.erase x.support a, if f x_1 = f a then ↑x x_1 else 0) = ↑x a
convert add_zero (x a)
case h.e'_2.h.e'_6
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
i : α
hi : i ∈ Finset.erase x.support a
⊢ ¬f i = f a
case h.e'_2.h.e'_6
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (∑ x_1 in Finset.erase x.support a, if f x_1 = f a then ↑x x_1 else 0) = 0
refine' Finset.sum_eq_zero fun i hi => if_neg _
no goals
case h.e'_2.h.e'_6
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
i : α
hi : i ∈ Finset.erase x.support a
⊢ ¬f i = f a
exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
case neg
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : ¬a ∈ x.support
⊢ (∑ x_1 in x.support, if f x_1 = f a then ↑x x_1 else 0) = 0
case neg
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : ¬a ∈ x.support
⊢ (∑ x_1 in x.support, if f x_1 = f a then ↑x x_1 else 0) = ↑x a
rw [not_mem_support_iff.1 hax]
case neg
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : ¬a ∈ x.support
i : α
hi : i ∈ x.support
⊢ ¬f i = f a
case neg
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : ¬a ∈ x.support
⊢ (∑ x_1 in x.support, if f x_1 = f a then ↑x x_1 else 0) = 0
refine' Finset.sum_eq_zero fun i hi => if_neg _
no goals
case neg
α : Type u_1
β : Type u_3
γ : Type ?u.190515
ι : Type ?u.190518
M : Type u_2
M' : Type ?u.190524
N : Type ?u.190527
P : Type ?u.190530
G : Type ?u.190533
H : Type ?u.190536
R : Type ?u.190539
S✝ : Type ?u.190542
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : ¬a ∈ x.support
i : α
hi : i ∈ x.support
⊢ ¬f i = f a
exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)