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
inst✝ : Fintype ι
m : M
i : ι
⊢ ↑(↑(toDual b) m) (↑b i) = ↑(equivFun b) m i
rw [b.equivFun_apply, toDual_eq_repr]