α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ ((sum (erase i f) fun a => g a) + sum (single i a) fun a => g a) + g i (↑f i) = sum f g + g i a
α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ sum (update f i a) g + g i (↑f i) = sum f g + g i a
rw [update_eq_erase_add_single, sum_add_index' hg hgg]
α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ ((sum (erase i f) fun a => g a) + sum (single i a) fun a => g a) + g i (↑f i) = sum (update f i (↑f i)) g + g i a
α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ ((sum (erase i f) fun a => g a) + sum (single i a) fun a => g a) + g i (↑f i) = sum f g + g i a
conv_rhs => rw [← Finsupp.update_self f i]
α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (sum (erase i f) fun a => g a) + ((sum (single i a) fun a => g a) + g i (↑f i)) =
    (sum (erase i f) fun a => g a) + ((sum (single i (↑f i)) fun a => g a) + g i a)
α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ ((sum (erase i f) fun a => g a) + sum (single i a) fun a => g a) + g i (↑f i) = sum (update f i (↑f i)) g + g i a
rw [update_eq_erase_add_single, sum_add_index' hg hgg, add_assoc, add_assoc]
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (sum (single i a) fun a => g a) + g i (↑f i) = (sum (single i (↑f i)) fun a => g a) + g i a
α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (sum (erase i f) fun a => g a) + ((sum (single i a) fun a => g a) + g i (↑f i)) =
    (sum (erase i f) fun a => g a) + ((sum (single i (↑f i)) fun a => g a) + g i a)
congr 1
no goals
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.285219
ι : Type u_3
M : Type ?u.285225
M' : Type ?u.285228
N : Type ?u.285231
P : Type ?u.285234
G : Type ?u.285237
H : Type ?u.285240
R : Type ?u.285243
S : Type ?u.285246
inst✝² : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (sum (single i a) fun a => g a) + g i (↑f i) = (sum (single i (↑f i)) fun a => g a) + g i a
rw [add_comm, sum_single_index (hg _), sum_single_index (hg _)]