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 のページを参照してください。

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