no goals
R : Type u_3
η : Type u_1
ιs : η → Type u_2
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
ji : (j : η) × ιs j
⊢ ↑(Pi.basis s).repr (↑(stdBasis R Ms ji.fst) (↑(s ji.fst) ji.snd)) = Finsupp.single ji 1
simp