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