Sets in Lean, sheet 6 : equality of sets #

Sets are extensional objects to mathematicians, which means that if two sets have the same elements, then they are equal.

Tactics #

Tactics you will need to know for this sheet:

• ext

The ext tactic #

If the goal is ⊢ A = B where A and B are subsets of X, then the tactic ext x, will create a hypothesis x : X and change the goal to x ∈ A ↔ x ∈ B.