# Using lean4 to prove subset properties

I'm learning Lean4.

I'm trying to prove in lean4 these basic properties of subsets:

1. $$X \subseteq X$$

2. $$X \subseteq Y , Y \subseteq Z \Rightarrow X \subseteq Z$$

3. $$X \subseteq Y , Y \subseteq X \Rightarrow X = Y$$

I'm wondering whether these translations in lean4 are correct:

import Mathlib.Data.Set.Lattice
variable {α : Type*}
open Set

variable {x y z: Set α}

example (h: x ⊆ x) : x ⊆ x := by
sorry

example (h: x ⊆ z) : x ⊆ y ∧ y ⊆ z := by
sorry

example (h: s = t) : x ⊆ y ∧ y ⊆ x := by
sorry

• All three examples are stated incorrectly. The first is trivially true. You are assuming what you are proving. The second you have the assumptions and the concluding reversed. The third is the same plus you have s and t. Commented Apr 13 at 12:22
• I rewrote my answer below to tell you the correct way to write these. Commented Apr 14 at 14:22

The correct way to write this is:

import Mathlib.Init.Set
variable {α : Type _}
variable {x y z: Set α}

example : x ⊆ x := by
intro a
sorry

example (h1 : x ⊆ y) (h2 : y ⊆ z) : x ⊆ z := by
intro a
sorry

example (h1 : x ⊆ y) (h2 : y ⊆ x) : x = y := by
funext a
apply propext
sorry


These are all in Mathlib already. You should be able to find them with the apply? tactic or http://moogle.ai .

But they are also good exercises. The main idea is that a set x : Set α is just a predicate α -> Prop and a ∈ x is just x a. So with this translation, x ⊆ y is just ∀ a : α, a ∈ x -> a ∈ y which is just ∀ a : α, x a -> y a. So to prove these, just pretend they are already translated into logic. I gave you some tactics to get you started.

• But perhaps stating the theorems properly will help the OP? Commented Apr 13 at 14:30
• Thank you for your reply @jason-rute, I have realised my mistakes. Commented Apr 14 at 17:29