by_cases

by_cases は排中律を使って場合分けをするタクティクです．by_cases h : P とすると，P が成り立つときと成り立たないときのゴールがそれぞれ生成されます．

example (P: Prop) : ¬¬P → P := by
  intro hnnP

  -- `P` が成り立つかどうかで場合分けする
  by_cases hP : P

  case pos =>
    -- `P` が成り立つとき
    assumption

  case neg =>
    -- `¬ P` が成り立つとき
    contradiction