by_contra

by_contra は，背理法を使いたいときに役立つタクティクです．

ゴールが ⊢ P であるときに by_contra h を実行すると，h : ¬ P がローカルコンテキストに追加されて，同時にゴールが ⊢ False になります．

import Mathlib.Tactic.ByContra

variable (P Q : Prop)

example (h: ¬Q → ¬P) : P → Q := by
  -- `P` であると仮定する
  intro hP

  -- `¬Q` であると仮定して矛盾を導きたい
  by_contra hnQ
  show False

  -- `¬ Q → ¬ P` と `¬Q` から `¬P` が導かれる
  have := h hnQ

  -- これは仮定に矛盾
  contradiction