no goals
l : Type ?u.141692
m : Type u_2
n : Type u_1
o : Type ?u.141701
m' : o → Type ?u.141706
n' : o → Type ?u.141711
R : Type ?u.141714
S : Type ?u.141717
α : Type v
β : Type w
γ : Type ?u.141724
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
x y : n → α
⊢ Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y
simp [dotProduct]