no goals
α : Type u_2
ι : Type ?u.265760
γ : Type ?u.265763
A : Type ?u.265766
B : Type ?u.265769
C : Type ?u.265772
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.268902
M : Type u_1
M' : Type ?u.268908
N : Type ?u.268911
P : Type ?u.268914
G : Type ?u.268917
H : Type ?u.268920
R : Type ?u.268923
S : Type ?u.268926
inst✝ : AddCommMonoid M
s✝ : Multiset M
a✝ : α
a : M
s : Multiset M
ih : single a✝ (Multiset.sum s) = Multiset.sum (Multiset.map (single a✝) s)
⊢ single a✝ (Multiset.sum (a ::ₘ s)) = Multiset.sum (Multiset.map (single a✝) (a ::ₘ s))
rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]