apply_assumption

apply_assumption は，ゴールが ⊢ head であるときに，... → ∀ _, ... → head という形の命題をローカルコンテキストから探し，それを用いてゴールを書き換えます．

variable (P Q R : Prop)

example (hPQ : P → Q) : ¬ Q → ¬ P := by
  intro hQn hP

  -- 矛盾を示したい
  show False

  -- 自動で `hQn` を適用
  apply_assumption
  show Q

  -- 自動で `hPQ` を適用
  apply_assumption
  show P

  -- 自動で `hP` を適用
  apply_assumption

  -- 証明終わり
  done

タクティクを繰り返すことを指示するタクティク repeat と組み合わせると，「ローカルコンテキストにある仮定を適切に選んで apply, exact することを繰り返し，ゴールを閉じる」ことができます．

example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
  repeat apply_assumption