Anatomy of a Lean proof for software engineers