This might be slightly controversial, but I think that one thing that would be valuable to formalize in Lean is the definition of a set.

Working mathematicians are used to formalizing things in terms of sets. Currently, I believe that requiring working mathematicians to swallow type theory before they can even get started with a theorem prover is a significant barrier to entry. It's just a hunch, but I think you'll get more buy-in from the mathematician in the street if you let them work set-theoretically.

Although I know that type-theoretic proof assistants have certain practical advantages, some people, such as John Harrison, have advocated a return to set theory.