Sets in Lean, example sheet 3 : not in (∉) #

The definition in Lean of x ∉ A is ¬ (x ∈ A). In other words, x ∉ A, ¬ (x ∈ A) and (x ∈ A) → false are all equal by definition in Lean. This means that they are all interchangeable, and you can change between them using the change tactic, or you can just keep this in mind. For example, if you have a hypothesis h : x ∉ A and your goal is false, then apply h will work and will change the goal to x ∈ A.

Tactics #

You can do all these levels just with intros, apply and exact!