no goals
R : Type ?u.2622120
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2622711
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ ↑(det e) (↑f ∘ v) = ↑LinearMap.det f * ↑(det e) v
rw [Basis.det_apply, Basis.det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
  e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
  e.constr_comp]