まとめ

Lean の基本は「すべての式には型がある」という考え方です． Prop は命題，Type はデータ型，Sort はその両方を含む一般化です． α → β と ∀ x : α, P x はどちらも関数型・依存関数型であり，命題として読むと含意や全称量化になります． inductive は constructor で項を作る型を定義し，structure は名前つき field をもつ積型を定義し，class は structure を型クラス探索に登録できる形で定義します．

Chapter 01 で見た P ∧ Q，P ∨ Q，∃ x, P x，a = b，¬ P，x ≤ y，x < y は，それぞれ And，Or，Exists，Eq，Not，LE.le，LT.lt の notation として理解できます． それぞれが structure，inductive，def，class のどれで実装されているかを見ると，constructor，cases，intro，rfl，rw などの tactic がどのような証明項を作っているかも見えやすくなります．

今後 Mathlib を読むときには，まず宣言が def なのか，theorem/lemma なのか，inductive なのか，structure なのか，class/instance なのかを見ると，対象の役割を把握しやすくなります．