cases'
cases'
は cases
に似ていますが lean3 の cases
に近い挙動をします。証明を構造化するため、 cases'
は使用しないことをお勧めします。
import Mathlib.Tactic.Cases -- `cases'` を使用するために必要
variable {P Q R : Prop}
example : P ∨ Q → (P → R) → (Q → R) → R := by
intro h hPR hQR
-- 場合分けをする
cases' h with hP hQ
· apply hPR hP
· apply hQR hQ