Proving that set A ≠ (Aᶜ)

Question

In Lean 4 I'm trying to prove that for any set it is the case that s ≠ (sᶜ), and got the following:

variable (s : Set α)

example (xInU: α) : s ≠ (sᶜ) := by
  intro n
  have ex : (xInU ∈ s) ∨ (xInU ∉ s) := em _
  have a1 : (xInU ∈ s) → False := fun inS => (n ▸ inS) inS
  have a2 : (xInU ∉ s) → False := fun ninS => (n ▸ ninS) ninS
  exact Or.elim ex a1 a2

I added the xInU hypothesis in order to have a witness for proceeding.

1. Can the proof be carried out without the xInU hypothesis?
2. Related, it is the case that Set.univ (for any type) have at least one element? (So a witness like xInU may always be put in context.) Maybe setting a "non empty" constraint to the α type?

Answer 1

Regarding your first question, no, if your type is empty then it's not true.

import Mathlib

example (h : ∀ (α : Type) (s : Set α), s ≠ sᶜ) : False := by
  apply h Empty ∅
  ext x
  cases x

In particular, the type Empty is an example of an empty type.

There is a predicate called Nonempty that can be used to say that a type is nonempty. It's a Prop so it's the mere fact that a type is nonempty, rather than giving an explicit witness. Here's a quick modification to your example to use it:

example [Nonempty α] : s ≠ (sᶜ) := by
  inhabit α
  let xInU : α := default
  intro n
  have ex : (xInU ∈ s) ∨ (xInU ∉ s) := em _
  have a1 : (xInU ∈ s) → False := fun inS => (n ▸ inS) inS
  have a2 : (xInU ∉ s) → False := fun ninS => (n ▸ ninS) ninS
  exact Or.elim ex a1 a2

Here's a shorter proof using some higher-powered tactics:

example [Nonempty α] : s ≠ (sᶜ) := by
  inhabit α
  intro n
  have n' := congr(default ∈ $n)
  tauto