∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : AddGroup α]
  (M N : (i : o) → Matrix (m' i) (n' i) α),
  Matrix.blockDiagonal' (M - N) = Matrix.blockDiagonal' M - Matrix.blockDiagonal' N