途中結果: have と suffices

have は証明の途中で補題を作ります． 長い証明では，途中結果に名前をつけると読みやすくなります． have h : Q := ... と書くと，以降の証明で h : Q を仮定として使えます．

show は現在のゴールを明示的に書き直すだけで，新しい仮定や途中結果は作りません． それに対して，have は新しい証明項に名前をつけてローカルコンテキストへ追加します．

example (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) (hP : P) : R := by
  have hQ : Q := hPQ hP
  exact hQR hQ

suffices h : Q は，「Q が示せれば現在のゴールが従う」という形で証明を組み替えます． 先に最終段階を宣言し，あとで十分条件を証明する書き方です． 証明の流れとしては，まず Q から元のゴールを導く部分を書き，その後で Q 自体を証明します． これも show とは異なり，現在のゴールを表示し直すのではなく，現在のゴールを「Q を示す」という新しいサブゴールに置き換えます．

example (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) (hP : P) : R := by
  suffices hQ : Q from hQR hQ
  exact hPQ hP