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