## More set theoretic proofs in Lean

We’ve seen an example where the goal is to give a proof of an equality of sets. Both in Lean and with pen-and-paper, to show two sets are equal `X=Y`

we use set extensionality to reduce to establishing `∀ x, x ∈ X ↔ x ∈ Y`

. We then take some `x ∈ U`

, prove one direction `x ∈ X → x ∈ Y`

, and then the other `x ∈ Y → x ∈ X`

.

While for pen-and-paper everyone can just do this conversion “in their head”, in Lean we need to step the computer through each time. This can be tedious so we automate it. For that, we can use a tactic called `set_extensionality`

.

`set_extensionality`

helps us when proving a goal of the form `X=Y`

. What if we have a hypothesis of set equality?

Rewriting the goal with the assumption `X=Y`

produces a new goal `X ∪ Z = X ∪ Z`

. Recall the tactic `rfl`

solves goals of the form `t = t`

. We can also use `rw`

in place of `rewrite`

and `rfl`

as `rw`

does a rewrite and then calls `rfl`

.

Let’s see another one.

The only thing left is to fill in the `sorry`

. Knowing that if `X ⊆ Y`

and `x ∉ Y`

, then `x ∉ X`

seems like a useful result itself. We give it a name and then use it. (Remember that given `h : A ∧ B`

we can access a proof of `A`

using `h.left`

and a proof of `B`

using `h.right`

.)

Next we look at the distributivity of intersection over unions.

In place of an `apply Or.elim`

, we have used the `cases`

tactic. This tactic creates different proof goals for each way there is to build the term. In our case, `h.right : x ∈ Y ∪ Z`

which is definitionally equivalent to `x ∈ Y ∨ x ∈ Z`

. There are two ways to make a proof of an or-statement: either you have a proof of the left and use `.inl`

or you have a proof the right and use `.inr`

. These constructors are the labels for the two branches of the cases. Note that `cases`

comes with additional syntax: `with`

and the `|`

to label the branches.

Here is an example with the use of `cases`

for the existential quantifer.