no goals
α : Type u_1
ι : Type ?u.632330
γ : Type ?u.632333
A : Type ?u.632336
B : Type ?u.632339
C : Type ?u.632342
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.635472
M : Type ?u.635475
M' : Type ?u.635478
N : Type ?u.635481
P : Type ?u.635484
G : Type ?u.635487
H : Type ?u.635490
R : Type u_2
S : Type u_3
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ b * sum s f = sum s fun a c => b * f a c
simp only [Finsupp.sum, Finset.mul_sum]