no goals
ι : Type u_4
ι' : Type ?u.704791
R : Type u_3
R₂ : Type ?u.704797
K : Type ?u.704800
M : Type u_2
M' : Type u_1
M'' : Type ?u.704809
V : Type u
V' : Type ?u.704814
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Fintype ι
b : Basis ι R M
S : Type u_5
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ↑(↑(constr b S) f) x = ∑ i : ι, ↑(equivFun b) x i • f i
simp [b.constr_apply, b.equivFun_apply, Finsupp.sum_fintype]