no goals
R : Type u_2
η : Type u_1
ιs : η → Type ?u.154579
Ms : η → Type ?u.154584
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
i : η
⊢ ↑(basisFun R η) i = ↑(stdBasis R (fun x => R) i) 1
simp only [basisFun, Basis.coe_ofEquivFun, LinearEquiv.refl_symm, LinearEquiv.refl_apply,
  stdBasis_apply]