no goals
ι✝ : Type ?u.612908
ι' : Type ?u.612911
R✝ : Type ?u.612914
R₂ : Type ?u.612917
K : Type ?u.612920
M : Type ?u.612923
M' : Type ?u.612926
M'' : Type ?u.612929
V : Type u
V' : Type ?u.612934
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
x : R
i : ι
⊢ ↑(↑(Basis.singleton ι R).repr x) i = x
simp [Basis.singleton, Unique.eq_default i]