no goals
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
i : ι
⊢ ↑(↑(toDual b) m) (↑b i) = ↑(↑b.repr m) i
rw [← b.toDual_total_left, b.total_repr]