Using lean4 to prove subset properties

Question

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

Answer 1

Edit: Rewrote answer.

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.