by を項の一部として使う

by は，証明全体だけでなく，項の一部としても使えます． Lean がある場所で型 T の項を期待しているなら，その場所に by ... と書いて tactic で項を作れます． たとえば P ∧ Q の証明は 2 つの成分を持つので，各成分の位置で小さな tactic 証明を書けます．

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
  ⟨by
      exact hP,
    by
      exact hQ⟩

example : {n : Nat // n < 3} :=
  ⟨2, by decide⟩

subtype の要素を作るには「値」と「その値が条件を満たす証明」が必要です． 上の例では，1 番目の成分が値 2，2 番目の成分が 2 < 3 の証明です． 後の章で出てくる ⟨2, by norm_num [ltThreeSet]⟩ も同じ形で，2 番目の成分だけを tactic で作っています．

名前つき定理でも，右辺に証明項を直接書けます． 短い証明では，この書き方の方が読みやすい場合があります．

theorem term_add_zero (n : Nat) : n + 0 = n :=
  Nat.add_zero n

tactic モードは「ゴールを変形する手続き」として読みやすく，証明項は「証明そのものを式として組み立てる」書き方です． 実際の開発では，短い証明は証明項で書き，長い証明や探索的な証明は tactic モードで書く，という使い分けがよくあります． ただしどちらの場合も，最終的には Lean のカーネルが証明項を型検査している点は同じです．