-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
inst_5 : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
simp_rw :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.reindexRange.repr : (a : M₁) → (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) →₀ R)
              ((f : (a : M₁) → M₁)
                ((v₁.reindexRange : (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → M₁)
                    (Subtype.mk (p := fun (x : M₁) ↦
                        Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
                        ((v₁ : (a : n) → M₁) i) ⋯ :
                      { x : M₁ //
                        Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
                  M₁)) :
            Finsupp.{u_5, u_1} (↑(Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) : Type u_5) R) :
          (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → R)
        (Subtype.mk (p := fun (x : M₁) ↦
            Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
            ((v₁ : (a : n) → M₁) k) ⋯ :
          { x : M₁ // Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
      R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) i : M₁)) : n →₀ R) : (a : n) → R) k : R)
simp_rw₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.reindexRange.repr : (a : M₁) → (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) →₀ R)
              ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) i : M₁)) :
            Finsupp.{u_5, u_1} (↑(Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) : Type u_5) R) :
          (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → R)
        (Subtype.mk (p := fun (x : M₁) ↦
            Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
            ((v₁ : (a : n) → M₁) k) ⋯ :
          { x : M₁ // Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
      R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((f : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) i : M₁)) : n →₀ R) : (a : n) → R) k : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrixAlgEquiv v₁.reindexRange :
          (a : M₁ →ₗ[R] M₁) →
            Matrix (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) R)
        f
        (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) k) ⋯)
        (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) i) ⋯) :
      R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f k i : R)

Tactic:
simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]

Premises used: Set.mem_range_self, Module.Basis.reindexRange_self, LinearMap.toMatrixAlgEquiv_apply, Module.Basis.reindexRange_repr