-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : Free R M
inst_6 : Free R M'
inst_7 : Module.Finite R M
inst_8 : Module.Finite R M'
f : End R M
f' : End R M'
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M') R M' := Free.chooseBasis R M'
rw :
  det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
      ((toMatrix (b.prod b') (b.prod b') :
          (a : M × M' →ₗ[R] M × M') →
            Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
              (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
        (prodMap f f')) =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
rw₁ :
  det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
      ((toMatrix (b.prod b') (b.prod b') :
          (a : M × M' →ₗ[R] M × M') →
            Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
              (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
        (prodMap f f')) =
    HMul.hMul (α := R) (β := R)
      (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) :
        R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
rw₂ :
  det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
      ((toMatrix (b.prod b') (b.prod b') :
          (a : M × M' →ₗ[R] M × M') →
            Matrix (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M')
              (Free.ChooseBasisIndex R M ⊕ Free.ChooseBasisIndex R M') R)
        (prodMap f f')) =
    HMul.hMul (α := R)
      (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))
      (det.{u_1, u_3} (n := Free.ChooseBasisIndex R M')
        ((toMatrix b' b' : (a : M' →ₗ[R] M') → Matrix (Free.ChooseBasisIndex R M') (Free.ChooseBasisIndex R M') R) f'))
rw₃ :
  det (n := Sum.{u_2, u_3} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M'))
      (fromBlocks
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) f) 0 0
        ((toMatrix b' b' : (a : M' →ₗ[R] M') → Matrix (Free.ChooseBasisIndex R M') (Free.ChooseBasisIndex R M') R)
          f')) =
    HMul.hMul (α := R)
      (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))
      (det.{u_1, u_3} (n := Free.ChooseBasisIndex R M')
        ((toMatrix b' b' : (a : M' →ₗ[R] M') → Matrix (Free.ChooseBasisIndex R M') (Free.ChooseBasisIndex R M') R) f'))
rw₄ :
  HMul.hMul (α := R)
      (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))
      (det.{u_1, u_3} (n := Free.ChooseBasisIndex R M')
        ((toMatrix b' b' : (a : M' →ₗ[R] M') → Matrix (Free.ChooseBasisIndex R M') (Free.ChooseBasisIndex R M') R)
          f')) =
    HMul.hMul (α := R)
      (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))
      (det.{u_1, u_3} (n := Free.ChooseBasisIndex R M')
        ((toMatrix b' b' : (a : M' →ₗ[R] M') → Matrix (Free.ChooseBasisIndex R M') (Free.ChooseBasisIndex R M') R) f'))
⊢ ((LinearMap.det (M := M × M') (A := R) : (M × M' →ₗ[R] M × M') →* R) : (a : M × M' →ₗ[R] M × M') → R) (prodMap f f') =
    HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
      ((LinearMap.det : (a : M' →ₗ[R] M') → R) f' : R)
have rw₅ : HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
    (det.{u_1, u_3} (n := Free.ChooseBasisIndex R M')
        ((toMatrix b' b' : (a : M' →ₗ[R] M') → Matrix (Free.ChooseBasisIndex R M') (Free.ChooseBasisIndex R M') R) f') :
      R) =
  HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
    (det.{u_1, u_3} (n := Free.ChooseBasisIndex R M')
        ((toMatrix b' b' : (a : M' →ₗ[R] M') → Matrix (Free.ChooseBasisIndex R M') (Free.ChooseBasisIndex R M') R) f') :
      R)
Tactic: rw [← det_toMatrix (b.prod b'), ← det_toMatrix b, ← det_toMatrix b', toMatrix_prodMap,
    det_fromBlocks_zero₂₁, det_toMatrix]