obtain

obtain は、分解して何かを得るときに使います。たとえばローカルコンテキストの h : P ∧ Q から hP : P と hQ : Q を取り出したり、h : ∃ e : X, P e から e : X と hP : P e を取り出したりすることができます。

基本的には obtain <パターン> : 型または命題 := 証明項 という構文で使用します。型は省略することができます。

-- 論理積の分解
example (P Q : Prop) (h : P ∧ Q) : True := by
  obtain ⟨hP, hQ⟩ : P ∧ Q := h

  -- 分解することができた
  guard_hyp hP : P
  guard_hyp hQ : Q

  trivial

-- P は X 上の述語
variable (X : Type) (P : X → Prop)

-- 存在命題の分解
example (h : ∃ e : X, P e) : True := by
  obtain ⟨e, hP⟩ := h

  -- 分解することができた
  guard_hyp e : X
  guard_hyp hP : P e

  trivial

obtain に与えることのできるパターンは rcases に与えられるパターンと同様で、一般の帰納型を分解することができます。

inductive Sample where
  | foo (x y : Nat)
  | bar (z : String)

example (s : Sample) : True := by
  obtain ⟨x, y⟩ | ⟨z⟩ := s

  case foo =>
    -- `x`, `y` が取り出せている
    guard_hyp x : Nat
    guard_hyp y : Nat

    trivial
  case bar =>
    -- `z` が取り出せている
    guard_hyp z : String

    trivial