-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
a :
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
              ((f i₂ : (a : M) → M) (if i₂ = j₂ then (b : (a : Free.ChooseBasisIndex R M) → M) j₁ else 0 : M)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
          (a : Free.ChooseBasisIndex R M) → R)
        i₁ :
      R)
    (if i₂ = j₂ then
        (((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f i₂ : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) j₁ : M)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i₁
      else 0 :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix
            (Basis.reindex
              (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
              (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M))
                (Equiv.prodComm ι (Free.ChooseBasisIndex R M))))
            (Basis.reindex
              (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
              (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M))
                (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))) :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) (i₁, i₂) (j₁, j₂) :
      R)
    (blockDiagonal
        (fun (i : ι) ↦
          (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i))
        (i₁, i₂) (j₁, j₂) :
      R)

Tactic:
simp_rw [LinearMap.toMatrix_apply', Matrix.blockDiagonal_apply, Basis.coe_reindex,
      Function.comp_apply, Basis.repr_reindex_apply, Equiv.symm_trans_apply, Equiv.prodComm_symm,
      Equiv.prodComm_apply, Equiv.sigmaEquivProd_symm_apply, Prod.swap_prod_mk, Pi.basis_apply,
      Pi.basis_repr, LinearMap.pi_apply, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.toMatrix_apply', LinearMap.coe_proj, Function.eval, Pi.single_apply]

Premises used: LinearMap.toMatrix_apply', Pi.single_apply, Pi.basis_apply, Equiv.sigmaEquivProd_symm_apply, Equiv.symm_trans_apply, LinearMap.coe_proj, LinearMap.pi_apply, Equiv.prodComm_apply, Prod.swap_prod_mk, Module.Basis.coe_reindex, Pi.basis_repr, Function.eval, Equiv.prodComm_symm, LinearMap.coe_comp, Function.comp_apply, Matrix.blockDiagonal_apply, Module.Basis.repr_reindex_apply