∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
  (D : Matrix n n α) [inst_5 : Invertible A], (Matrix.fromBlocks A B C D).det = A.det * (D - C * ⅟A * B).det