no goals
ι : Type u_1
ι' : Type ?u.687118
R : Type u_2
R₂ : Type ?u.687124
K : Type ?u.687127
M : Type u_3
M' : Type ?u.687133
M'' : Type ?u.687136
V : Type u
V' : Type ?u.687141
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Fintype ι
b : Basis ι R M
inst✝ : DecidableEq ι
e : M ≃ₗ[R] ι → R
i j : ι
⊢ ↑e (↑(ofEquivFun e) i) j = ↑e (↑(LinearEquiv.symm e) (update 0 i 1)) j
simp [Basis.ofEquivFun, ← Finsupp.single_eq_pi_single, Finsupp.single_eq_update]