by

Lean においては，命題は型で，証明はその項です．命題 P の証明を構成するとは項 h : P を構成するということです．by は，証明の構成をタクティクで行いたいときに使います．

証明項による証明とは，たとえば次のようなものです．

variable (P Q R : Prop)

-- `P → R` というのは `P` の証明を与えられたときに `R` の証明を返す関数の型
-- したがって，その証明は関数となる
example (hPQ : P → Q) (hQR : Q → R) : P → R :=
  fun hP ↦ hQR (hPQ hP)

同じ命題をタクティクを使って示すと，例えば次のようになります．

-- 同じ命題をタクティクで示した例
example (hPQ : P → Q) (hQR : Q → R) : P → R := by
  intro hP
  exact hQR (hPQ hP)

by?

by の代わりに by? を使うとタクティクモードで構成した証明を直接構成した証明に変換してくれます.show_term by としてもほぼ同じ結果が得られます．

example (hPQ : P → Q) (hQR : Q → R) : P → R := by?
  -- `Try this: fun hP => hQR (hPQ hP)` と提案してくれる
  intro hP
  exact hQR (hPQ hP)

/-- info: Try this: fun hP => hQR (hPQ hP) -/
#guard_msgs in
example (hPQ : P → Q) (hQR : Q → R) : P → R := show_term by
  intro hP
  exact hQR (hPQ hP)