-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_8 : DecidableEq M₁
f : M₁ →ₗ[R] M₂
k : m
i : n
simp_rw :
  Eq.{u_1 + 1} (α := R)
    ((((v₂.reindexRange.repr : (a : M₂) → (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6) →₀ 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_6, u_1} (↑(Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) : Type u_6) R) :
          (a : (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6)) → R)
        (Subtype.mk (p := fun (x : M₂) ↦
            Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x)
            ((v₂ : (a : m) → M₂) k) ⋯ :
          { x : M₂ // Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x }) :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) i : M₁)) : m →₀ R) : (a : m) → R) k : R)
simp_rw₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₂.reindexRange.repr : (a : M₂) → (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6) →₀ R)
              ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) i : M₁)) :
            Finsupp.{u_6, u_1} (↑(Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) : Type u_6) R) :
          (a : (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6)) → R)
        (Subtype.mk (p := fun (x : M₂) ↦
            Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x)
            ((v₂ : (a : m) → M₂) k) ⋯ :
          { x : M₂ // Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x }) :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) i : M₁)) : m →₀ R) : (a : m) → R) k : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix v₁.reindexRange v₂.reindexRange :
          (a : M₁ →ₗ[R] M₂) →
            Matrix (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6) (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) R)
        f
        (Subtype.mk (p := fun (x : M₂) ↦
          Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x)
          ((v₂ : (a : m) → 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)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f k i : R)

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

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