Dealing with Laws of Excluded Middle in Lean

user_15111056 0
Viewed 93
section
open classical
example : ¬ (A ↔ ¬ A) :=
have hn : (A ∨ ¬ A), from sorry,
  assume h : (A ↔ ¬ A),
  show false, from or.elim hn
    (assume h1 : A, h.mp h1 h1)
    (assume h2 : ¬ A, h2 (h.mpr h2))
end

I am studying Lean with Jeremy Avigad's book Logic and Proof. The problem is that I have to deal with Laws of Excluded Middle only with by_contradiction tactic. Can someone help me out?

lean
0 Answers
Related