-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
let let₁ let₂ let₃ :
  Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := (i : ι) → M) (A := R) : (((i : ι) → M) →ₗ[R] (i : ι) → M) →* R) :
          (a : ((i : ι) → M) →ₗ[R] (i : ι) → M) → R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i :
          ((i : ι) → M) →ₗ[R] (i : ι) → M) :
      R)
    (∏ i : ι, (LinearMap.det : (a : M →ₗ[R] M) → R) (f i) : R)
let₄ :
  let b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M;
  let 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)));
  Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i)))
    (∏ x : ι,
      det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := (i : ι) → M) (A := R) : (((i : ι) → M) →ₗ[R] (i : ι) → M) →* R) :
          (a : ((i : ι) → M) →ₗ[R] (i : ι) → M) → R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i :
          ((i : ι) → M) →ₗ[R] (i : ι) → M) :
      R)
    (∏ i : ι, (LinearMap.det : (a : M →ₗ[R] M) → R) (f i) : R)
have let₅ : let b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M;
let 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)));
∀
  (this :
    Eq (α := Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
      ((toMatrix B B :
            (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) :
        Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
      (blockDiagonal fun (i : ι) ↦
          (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i) :
        Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)),
  Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i)))
    (∏ x : ι,
      det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f x)))
Tactic: classical
  let b := Module.Free.chooseBasis R M
  let B := (Pi.basis (fun _ : ι ↦ b)).reindex <|
    (Equiv.sigmaEquivProd _ _).trans (Equiv.prodComm _ _)
  simp_rw [← LinearMap.det_toMatrix B, ← LinearMap.det_toMatrix b]
  have : ((LinearMap.toMatrix B B) (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)) =
      Matrix.blockDiagonal (fun i ↦ LinearMap.toMatrix b b (f i)) := by
    ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
    unfold B
    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]
    split_ifs with h
    · rw [h]
    · simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]
  rw [this, Matrix.det_blockDiagonal]