no goals
l : Type ?u.134471
m : Type u_1
n : Type ?u.134477
o : Type ?u.134480
m' : o → Type ?u.134485
n' : o → Type ?u.134490
R : Type ?u.134493
S : Type ?u.134496
α : Type v
β : Type w
γ : Type ?u.134503
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
⊢ (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w
simp [dotProduct, add_mul, Finset.sum_add_distrib]