#find はライブラリ検索を行うコマンドです。
#find
Lean 実行環境で実行せずとも、Loogle というウェブサイトがあり、ここで #find を実行することができます。詳細な解説もそちらに譲ります。
また、Mathlib の検索では Moogle というサイトもあります。こちらは自然言語検索が可能です。