no goals
α : Type u
β : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
b : β
f✝ g✝ : α → β
inst✝ : NonUnitalNonAssocSemiring β
n k : ℕ
f g : ℕ → β
⊢ (∑ i in range (n + 1), f i) * ∑ i in range (k + 1), g i =
    (∑ i in range n, f i) * ∑ i in range k, g i + f n * ∑ i in range k, g i + (∑ i in range n, f i) * g k + f n * g k
simp only [add_mul, mul_add, add_assoc, sum_range_succ]