no goals
α : Type u_4
ι : Type u_2
γ : Type ?u.618499
A : Type u_3
B : Type ?u.618505
C : Type u_1
inst✝² : AddCommMonoid A
inst✝¹ : AddCommMonoid B
inst✝ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s✝ : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.621638
M : Type ?u.621641
M' : Type ?u.621644
N : Type ?u.621647
P : Type ?u.621650
G : Type ?u.621653
H : Type ?u.621656
R : Type ?u.621659
S : Type ?u.621662
a : α
s : Finset α
has : ¬a ∈ s
ih : sum (∑ x in s, f x) t = ∑ x in s, sum (f x) t
⊢ sum (∑ x in insert a s, f x) t = ∑ x in insert a s, sum (f x) t
simp_rw [Finset.sum_insert has, Finsupp.sum_add_index' h0 h1, ih]