まとめ

tactic モードでは，現在のゴールとローカルコンテキストを見ながら，証明を小さなステップに分解します． intro と apply は含意や全称命題，rw，simp，calc は等式や計算，constructor，match，cases，induction は structure や inductive 型に対応します．

外延性を使う funext や ext，矛盾を扱う exfalso，contradiction，背理法は数学でよく使うため，基本 tactic の次に押さえておくと便利です． conv，等号パターンの総整理，古典論理・選択・商などの追加原理は，証明が複雑になったときに参照する後半の話題として位置づけています．