no goals
ι : Type u_4
R : Type u_1
S : Type ?u.308054
M : ι → Type u_2
N : Type u_3
dec_ι : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : (x : N) → Decidable (x ≠ 0)
f : (i : ι) → M i →ₗ[R] N
i : ι
x : M i
⊢ ↑(coprodMap f) (single i x) = ↑(f i) x
simp [coprodMap_apply]