no goals
α : Type u_1
M : Type u_3
N : Type ?u.323475
P : Type ?u.323478
R : Type u_2
S : Type ?u.323484
inst✝¹³ : Semiring R
inst✝¹² : Semiring S
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
α' : Type ?u.323576
M' : Type ?u.323579
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M
inst✝² : Module R M'
inst✝¹ : Module R M
v✝ : α → M
v' : α' → M'
inst✝ : Unique α
l : α →₀ R
v : α → M
⊢ ↑(Finsupp.total α M R v) l = ↑l default • v default
rw [← total_single, ← unique_single l]