assumption

assumption は，現在のゴール ⊢ P がローカルコンテキストにあるとき，ゴールを閉じます．

variable (P Q : Prop)

example (hP: P) (_: Q) : P := by
  assumption

assumption による証明は，どの仮定を使うか明示すれば exact で書き直すことができます．assumption を使用することにより，仮定の名前の変更に対してロバストになるほか，意図がわかりやすくなるというメリットがあります．

example (hP: P) (_: Q) : P := by
  exact hP