done

done は，証明終了の合図です．証明すべきゴールが残っていない時に成功し，それ以外の時にはエラーになります．QED のようなものです．証明がサブゴールに分かれている場合，サブゴールごとに判定を行います．

variable (P Q : Prop)

example (h : P → Q) : ¬ P ∨ Q := by
  -- `P` が成り立つかどうかで場合分けを行う
  by_cases hP : P

  -- `P` が成り立つ場合
  case pos =>
    -- `P → Q` より `Q` が成り立つ
    have := h hP

    -- したがって結論が従う
    exact Or.inr this

    -- `P` が成り立つ場合の証明終わり.
    done

  -- `P` が成り立たない場合
  case neg =>
    -- `¬ P` が成り立つので，`¬ P ∨ Q` も成り立つ
    exact Or.inl hP

    -- `P` が成り立たない場合の証明終わり.
    done