#find

#find はライブラリ検索を行うコマンドです。

Lean 実行環境で実行せずとも、Loogle というウェブサイトがあり、ここで #find を実行することができます。詳細な解説もそちらに譲ります。

また、Mathlib の検索では Moogle というサイトもあります。こちらは自然言語検索が可能です。