まとめ

命題論理の基本規則は，Lean では intro，exact，constructor，cases，False.elim などに対応します． 述語論理では，∀ を関数のように適用し，∃ を証拠とその証明の組として扱います． 以降の数学の形式化では，これらの規則を明示的に使うだけでなく，rw，simp，apply などのタクティックで同じ推論をより短く書くこともあります．