no goals
R : Type u_1
η : Type u_2
ιs : η → Type ?u.157855
Ms : η → Type ?u.157860
inst✝³ : Semiring R
inst✝² : (i : η) → AddCommMonoid (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : Fintype η
x : η → R
i : η
⊢ ↑(↑(basisFun R η).repr x) i = x i
simp [basisFun]