no goals
R : Type u_3
inst✝⁹ : CommSemiring R
l : Type ?u.1797707
m : Type u_4
n : Type u_5
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝¹ : DecidableEq M₁
inst✝ : DecidableEq M₂
f : M₁ →ₗ[R] M₂
k : m
i : n
⊢ ↑(toMatrix (Basis.reindexRange v₁) (Basis.reindexRange v₂)) f
      { val := ↑v₂ k, property := (_ : ↑v₂ k ∈ Set.range ↑v₂) }
      { val := ↑v₁ i, property := (_ : ↑v₁ i ∈ Set.range ↑v₁) } =
    ↑(toMatrix v₁ v₂) f k i
simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]