検索系: #check，exact?，rw?

使える補題を探すことは，Lean で数学を形式化するときの大きな作業です．

#check

名前が分かっている定理の型を確認します． 定理名が分かっている場合は #check，現在のゴールから候補を探したい場合は exact?，rw? のような検索支援を使い分けます．

#check Nat.add_comm
#check Nat.add_assoc

exact?，rw?，try?

現在のゴールを閉じる候補や書き換え候補を提案する tactic です． 出力は Lean のバージョンや読み込んだライブラリによって変わることがあるため，この資料では実行例としてだけ示します．

example (n : Nat) : n + 0 = n := by
  exact?

example (a b : Nat) : a + b = b + a := by
  rw?

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  try?

Mathlib には #loogle などのより強力な検索支援もあります． それらは次章以降，Mathlib を使う場面で扱います．