no goals
ι : Type u_2
ι' : Type ?u.516785
R : Type u_3
R₂ : Type ?u.516791
K : Type ?u.516794
M : Type u_4
M' : Type u_1
M'' : Type ?u.516803
V : Type u
V' : Type ?u.516808
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
S : Type u_5
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
i : ι
⊢ ↑(↑(constr b S) f) (↑b i) = f i
simp [Basis.constr_apply, b.repr_self]