no goals
α : Type u_1
ι : Type ?u.627194
γ : Type ?u.627197
A : Type ?u.627200
B : Type ?u.627203
C : Type ?u.627206
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.630336
M : Type ?u.630339
M' : Type ?u.630342
N : Type ?u.630345
P : Type ?u.630348
G : Type ?u.630351
H : Type ?u.630354
R : Type u_2
S : Type u_3
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : α →₀ R
f : α → R → S
⊢ sum s f * b = sum s fun a c => f a c * b
simp only [Finsupp.sum, Finset.sum_mul]