Lean 2

Lean による定理証明に関する素振り．
今回は次の命題を証明する．

⊢ の右側に表示されている現在証明すべき命題は Q ．まず，仮定 h : P → Q を適用すると，

⊢ の右側に P が表示される．
続けて，仮定 hP : P を適用すると，

No goals となる．これで証明完了．

なお，2つの仮定の適用は次のように1行にまとめることもできる．

example (h : P → Q) (hP : P) : Q := by
  apply h hP