#find

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

Lean 実行環境で実行せずとも、Loogle というウェブサイトがあり、ここで #find を実行することができます。そして #loogle コマンドで Loogle をエディタから利用することができるので、使用法の解説はそちらに譲ります。

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