no goals
ι : Type u_3
ι' : Type ?u.1271219
R : Type u_2
R₂ : Type ?u.1271225
K : Type ?u.1271228
M : Type u_1
M' : Type ?u.1271234
M'' : Type ?u.1271237
V : Type u
V' : Type ?u.1271242
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
i : ι
⊢ ↑(↑(restrictScalars R b) i) = ↑b i
simp only [Basis.restrictScalars, Basis.span_apply]