no goals
α : Type u_3
ι : Type ?u.559428
γ : Type ?u.559431
A : Type ?u.559434
B : Type ?u.559437
C : Type ?u.559440
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.562570
M : Type u_1
M' : Type ?u.562576
N : Type u_2
P : Type ?u.562582
G : Type ?u.562585
H : Type ?u.562588
R : Type ?u.562591
S : Type ?u.562594
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : sum (Multiset.sum s) h = Multiset.sum (Multiset.map (fun g => sum g h) s)
⊢ sum (Multiset.sum (a ::ₘ s)) h = Multiset.sum (Multiset.map (fun g => sum g h) (a ::ₘ s))
rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]