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