We will talk about using Lean to provide guarantees about data structures which are useful real world software. In particular, we will look at arrays and vectors. The arrays require a proof obligation for access at a given index. The vectors have their size included in its type. Additionally, we will show how to use the Lean tooling to configure, build, and run a small program.