How to do it properly in lean

Stream: new members

[Chris B]

@T.X. Xia

Here's one that's more compact, but I don't necessarily think there's a "right way", yours is fine. Some people prefer using tactic mode for these kinds of propositional shuffling exercises.

example (p : α → Prop) : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
  Iff.intro
    (fun ⟨x, hpx⟩ h => h x hpx)
    (fun hna => Classical.byContradiction $ fun hne => hna (fun x hpx => absurd ⟨x, hpx⟩ hne))

The doc generation stuff for lean 4 is still a wip, but there's a hosted instance of the prelude/std/mathlib docs on the leanprover-community site. The Classical section is here: https://leanprover-community.github.io/mathlib4_docs/Init/Classical.html

Classical is just a namespace which can be split up, so you can't directly go to def in vscode, but for specific definitions you should be able to right click and go to definition.

[Chris B]

There's also a lot of interplay between decidable and classical, so some declarations that might be of interest are probably in other sections like Mathlib.Logic.Basic.