no goals
ι : Type u_5
R : Type u_3
S : Type u_1
M : ι → Type u_4
N : Type u_2
dec_ι : DecidableEq ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M i)
inst✝⁵ : (i : ι) → Module R (M i)
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
i : ι
x : M i
⊢ ↑(↑(lsum S) F) (single i x) = ↑(F i) x
simp