no goals
ι✝ : Type ?u.609084
ι' : Type ?u.609087
R✝ : Type ?u.609090
R₂ : Type ?u.609093
K : Type ?u.609096
M : Type ?u.609099
M' : Type ?u.609102
M'' : Type ?u.609105
V : Type u
V' : Type ?u.609110
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b b₁ : Basis ι✝ R✝ M
i✝ : ι✝
c : R✝
x : M
ι : Type u_1
R : Type u_2
inst✝¹ : Unique ι
inst✝ : Semiring R
i : ι
⊢ ↑(Basis.singleton ι R).repr 1 = Finsupp.single i 1
simp [Basis.singleton]