no goals
ι : Type u_4
ι' : Type ?u.538910
R : Type u_1
R₂ : Type ?u.538916
K : Type ?u.538919
M : Type u_3
M' : Type u_2
M'' : Type ?u.538928
V : Type u
V' : Type ?u.538933
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' →ₗ[R] M'
v : ι → M'
i : ι
⊢ ↑(↑(constr b S) (↑f ∘ v)) (↑b i) = ↑(LinearMap.comp f (↑(constr b S) v)) (↑b i)
simp only [Basis.constr_basis, LinearMap.comp_apply, Function.comp]