Lean 6

萩原先生から出題された課題（脳トレ）を解いてみた．

import Mathlib.Tactic

section
  variable (A : Prop)
  example : ¬ (A ↔ ¬ A) := by
    intro (h : A ↔ ¬ A)
    have h1 : A → ¬ A := h.mp
    have h2 : ¬ A → A := h.mpr
    have h3 : (A → ¬ A) → ¬ A := by
      intro (hana : A → ¬ A) (ha : A)
      apply hana ha
      apply ha
    have ha : A := h2 (h3 h1)
    have hna : ¬ A := h1 ha
    exact hna ha
end

-- 以下の飛び道具（定理）を使った別解
-- imp_not_self {a : Prop} : a → ¬a ↔ ¬a
-- not_imp_self {a : Prop} : ¬a → a ↔ a
section -- 2023-10-30
  variable (A : Prop)
  example : ¬ (A ↔ ¬ A) := by
    intro (h : A ↔ ¬ A)
    have h1 : A → ¬ A := h.mp
    have h2 : ¬ A → A := h.mpr
    simp only [imp_not_self, not_imp_self] at h1 h2 -- (h1 : ¬ A) (h2 : A) にする．
    exact h1 h2
end