まとめ

Mathlib を使う証明では，具体的な対象だけでなく，それが持つ型クラスインスタンスを意識することが重要です． Set α は型 α 上の部分集合全体を表し，Finset α は有限集合をデータとして持つ型です． また，ℝ，ℝ≥0，ℝ≥0∞，EReal は別々の型であり，用途に応じて選びます． それぞれに登録された型クラスインスタンスと，型の間の coercion・変換関数を確認することが重要です． 不等式 a ≤ b や a < b は，両辺の型に入っている順序構造から作られる命題です． 数値計算，線形不等式，多項式不等式，単調性，型変換を切り分けると，使う tactic や補題を選びやすくなります．

Mathlib の証明は既存補題の組み合わせです． #check，#synth，命名規則，simp，rw，ext，norm_num，linarith，nlinarith を使いながら，ゴールに合う補題を探して適用します． 大きな流れとしては，まず型クラスや bundled structure などの一般的な読み方を押さえ，その上で Set，Finset，実数，不等式の各対象に入ると，Mathlib の定理の形が見通しやすくなります．