Fundamentals

Analysis I, Section 3.1: Fundamentals (of set theory)

In this section we set up a version of Zermelo-Frankel set theory (with atoms) that tries to be as faithful as possible to the original text of Analysis I, Section 3.1. All numbering refers to the original text.

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

A type Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.SetTheory.Set of sets
A type Chapter3.SetTheory.Object.{u, v} [self : Chapter3.SetTheory] : Type vChapter3.SetTheory.Object of objects
An axiom that every set is (or can be coerced into) an object
The empty set ∅ : ?m.1∅, singletons overloaded, errors 1:1 Unknown identifier `y` invalid {...} notation, expected type is not known{y}, and pairs overloaded, errors 1:1 Unknown identifier `y` invalid {...} notation, expected type is not known{y,z} (and more general finite tuples), with their attendant axioms
Pairwise union Unknown identifier `X`sorry ∪ sorry : ?m.1X ∪ Unknown identifier `Y`Y, and their attendant axioms
Coercion of a set Unknown identifier `A`A to its associated type Unknown identifier `A.toSubtype`A.toSubtype, which is a subtype of Unknown identifier `Object`Object, and basic API. (This is a technical construction needed to make the Zermelo-Frankel set theory compatible with the dependent type theory of Lean.)
The specification Unknown identifier `A.specify`A.specify P of a set Unknown identifier `A`A and a predicate to the subset of elements of Unknown identifier `A`A obeying Unknown identifier `P`P, and the axiom of specification. TODO: somehow implement set builder elaboration for this.
The replacement Unknown identifier `A.replace`A.replace hP of a set Unknown identifier `A`A via a predicate obeying a uniqueness condition ∀ (x : ?m.1) (y y' : ?m.6 x), sorry ∧ sorry → y = y' : Prop∀ x y y', Unknown identifier `P`P x y ∧ Unknown identifier `P`P x y' → y = y', and the axiom of replacement.
A bijective correspondence between the Mathlib natural numbers ℕ : Typeℕ and a set (the axiom of infinity).
Axioms of regularity, power set, and union (used in later sections of this chapter, but not required here)
Connections with Mathlib's notion of a set

The other axioms of Zermelo-Frankel set theory are discussed in later sections.

Some technical notes:

Mathlib of course has its own notion of a Set.{u} (α : Type u) : Type uSet (or more precisely, a type Set sorry : Type u_1Set Unknown identifier `X`X associated to each type Unknown identifier `X`X), which is not compatible with the notion Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.Set defined here, though we will try to make the notations match as much as possible. This causes some notational conflict: for instance, one may need to explicitly specify (∅:failed to synthesize Chapter3.SetTheory Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Chapter3.Set) instead of just ∅ : ?m.1∅ to indicate that one is using the Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.Set version of the empty set, rather than the Mathlib version of the empty set, and similarly for other notation defined here.
In Analysis I, we chose to work with an "impure" set theory, in which there could be more Unknown identifier `Object`Objects than just Set.{u} (α : Type u) : Type uSets. In the type theory of Lean, this requires treating Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.Set and Chapter3.SetTheory.Object.{u, v} [self : Chapter3.SetTheory] : Type vChapter3.Object as distinct types. Occasionally this means we have to use a coercion (Unknown identifier `X`X: failed to synthesize Chapter3.SetTheory Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Chapter3.Object) of a Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.Set Unknown identifier `X`X to make into a Chapter3.SetTheory.Object.{u, v} [self : Chapter3.SetTheory] : Type vChapter3.Object: this is mostly needed when manipulating sets of sets.
Strictly speaking, a set is not a type; however, we will coerce sets to types, and specifically to a subtype of Unknown identifier `Object`Object. A similar coercion is in place for Mathlib's formalization of sets.
After this chapter is concluded, the notion of a Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.SetTheory.Set will be deprecated in favor of the standard Mathlib notion of a Set.{u} (α : Type u) : Type uSet (or more precisely of the type Set sorry : Type u_1Set Unknown identifier `X`X of a set in a given type Unknown identifier `X`X). However, due to various technical incompatibilities between set theory and type theory, we will not attempt to create a full equivalence between these two notions of sets. (As such, this makes this entire chapter optional from the point of view of the rest of the book, though we retain it for pedagogical purposes.)

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

namespace Chapter3

/- The ability to work in multiple universe is not relevant immediately, but
becomes relevant when constructing models of set theory in the Chapter 3 epilogue. -/
universe u v

The axioms of Zermelo-Frankel theory with atoms.

class SetTheory where
  Set : Type u -- Axiom 3.1
  Object : Type v -- Axiom 3.1
  set_to_object : Set ↪ Object -- Axiom 3.1
  mem : Object → Set → Prop -- Axiom 3.1
  extensionality X Y : (∀ x, mem x X ↔ mem x Y) → X = Y -- Axiom 3.2
  emptyset: Set -- Axiom 3.3
  emptyset_mem x : ¬ mem x emptyset -- Axiom 3.3
  singleton : Object → Set -- Axiom 3.4
  singleton_axiom x y : mem x (singleton y) ↔ x = y -- Axiom 3.4
  union_pair : Set → Set → Set -- Axiom 3.5
  union_pair_axiom X Y x : mem x (union_pair X Y) ↔ (mem x X ∨ mem x Y) -- Axiom 3.5
  specify A (P: Subtype (mem .A) → Prop) : Set -- Axiom 3.6
  specification_axiom A (P: Subtype (mem .A) → Prop) :
    (∀ x, mem x (specify A P) → mem x A) ∧ ∀ x, mem x.val (specify A P) ↔ P x -- Axiom 3.6
  replace A (P: Subtype (mem .A) → Object → Prop)
    (hP: ∀ x y y', P x y ∧ P x y' → y = y') : Set -- Axiom 3.7
  replacement_axiom A (P: Subtype (mem .A) → Object → Prop)
    (hP: ∀ x y y', P x y ∧ P x y' → y = y') : ∀ y, mem y (replace A P hP) ↔ ∃ x, P x y -- Axiom 3.7
  nat : Set -- Axiom 3.8
  nat_equiv : ℕ ≃ Subtype (mem .nat) -- Axiom 3.8
  regularity_axiom A (hA : ∃ x, mem x A) :
    ∃ x, mem x A ∧ ∀ S, x = set_to_object S → ¬ ∃ y, mem y A ∧ mem y S -- Axiom 3.9
  pow : Set → Set → Set -- Axiom 3.11
  function_to_object (X: Set) (Y: Set) :
    (Subtype (mem .X) → Subtype (mem .Y)) ↪ Object -- Axiom 3.11
  powerset_axiom (X: Set) (Y: Set) (F:Object) :
    mem F (pow X Y) ↔ ∃ f: Subtype (mem .Y) → Subtype (mem .X),
    function_to_object Y X f = F -- Axiom 3.11
  union : Set → Set -- Axiom 3.12
  union_axiom A x : mem x (union A) ↔ ∃ S, mem x S ∧ mem (set_to_object S) A -- Axiom 3.12

-- This enables one to use `Set` and `Object` instead of `SetTheory.Set` and `SetTheory.Object`.
export SetTheory (Set Object)

-- This instance implicitly imposes the axioms of Zermelo-Frankel set theory with atoms.
variable [SetTheory]

Definition 3.1.1 (objects can be elements of sets)

instance SetTheory.objects_mem_sets : Membership Object Set where
  mem X x := mem x X

-- Now we can use the `∈` notation between our `Object` and `Set`.
example (X: Set) (x: Object) : x ∈ X ↔ SetTheory.mem x X := byinst✝:SetTheoryX:Setx:Object⊢ x ∈ X ↔ SetTheory.mem x X rflAll goals completed! 🐙

Axiom 3.1 (Sets are objects)

instance SetTheory.sets_are_objects : Coe Set Object where
  coe X := set_to_object X

-- Now we can treat a `Set` as an `Object` when needed.
example (X: Set) : (X: Object) = SetTheory.set_to_object X := rfl

Axiom 3.1 (Sets are objects)

theorem SetTheory.Set.coe_eq {X Y:Set} (h: (X: Object) = (Y: Object)) : X = Y :=
  set_to_object.inj' h

Axiom 3.1 (Sets are objects)

@[simp]
theorem SetTheory.Set.coe_eq_iff (X Y:Set) : (X: Object) = (Y: Object) ↔  X = Y :=
  ⟨ coe_eq, byinst✝:SetTheoryX:SetY:Set⊢ X = Y → set_to_object X = set_to_object Y rintro rflinst✝:SetTheoryX:Set⊢ set_to_object X = set_to_object X; rflAll goals completed! 🐙 ⟩

Axiom 3.2 (Equality of sets). The [sorry] : List ?m.2[Unknown identifier `ext`ext] tag allows the Unknown identifier `ext`ext tactic to work for sets.

@[ext]
theorem SetTheory.Set.ext {X Y:Set} (h: ∀ x, x ∈ X ↔ x ∈ Y) : X = Y := extensionality _ _ h

Chapter3.SetTheory.Set.ext_iff.{u_1, u_2} [SetTheory] {X Y : Set} : X = Y ↔ ∀ (x : Object), x ∈ X ↔ x ∈ Y

instance SetTheory.Set.instEmpty : EmptyCollection Set where
  emptyCollection := emptyset

-- Now we can use the `∅` notation to refer to `SetTheory.emptyset`.
example : ∅ = SetTheory.emptyset := rfl

-- Make everything we define in `SetTheory.Set.*` accessible directly.
open SetTheory.Set

Axiom 3.3 (empty set). Note: in some applications one may have to explicitly cast ∅ to Set due to Mathlib's existing set theory notation.

@[simp]
theorem SetTheory.Set.not_mem_empty : ∀ x, x ∉ (∅:Set) := emptyset_mem

Empty set has no elements

theorem declaration uses 'sorry'SetTheory.Set.eq_empty_iff_forall_notMem {X:Set} : X = ∅ ↔ (∀ x, x ∉ X) := byinst✝:SetTheoryX:Set⊢ X = ∅ ↔ ∀ (x : Object), x ∉ X
  sorryAll goals completed! 🐙

Empty set is unique

theorem declaration uses 'sorry'SetTheory.Set.empty_unique : ∃! (X:Set), ∀ x, x ∉ X := byinst✝:SetTheory⊢ ∃! X, ∀ (x : Object), x ∉ X
  sorryAll goals completed! 🐙

Lemma 3.1.5 (Single choice)

lemma SetTheory.Set.nonempty_def {X:Set} (h: X ≠ ∅) : ∃ x, x ∈ X := byinst✝:SetTheoryX:Seth:X ≠ ∅⊢ ∃ x, x ∈ X
  -- This proof is written to follow the structure of the original text.
  by_contra! thisinst✝:SetTheoryX:Seth:X ≠ ∅this:∀ (x : Object), x ∉ X⊢ False
  have claim (x:Object) : x ∈ X ↔ x ∈ (∅:Set) := byinst✝:SetTheoryX:Seth:X ≠ ∅⊢ ∃ x, x ∈ X simp [this, not_mem_empty]All goals completed! 🐙
  apply ext at claiminst✝:SetTheoryX:Seth:X ≠ ∅this:∀ (x : Object), x ∉ Xclaim:X = ∅⊢ False
  contradictionAll goals completed! 🐙

theorem SetTheory.Set.nonempty_of_inhabited {X:Set} {x:Object} (h:x ∈ X) : X ≠ ∅ := byinst✝:SetTheoryX:Setx:Objecth:x ∈ X⊢ X ≠ ∅
  contrapose! hinst✝:SetTheoryX:Setx:Objecth:X = ∅⊢ x ∉ X
  rw [eq_empty_iff_forall_notMem] at hinst✝:SetTheoryX:Setx:Objecth:∀ (x : Object), x ∉ X⊢ x ∉ X
  exact h xAll goals completed! 🐙

instance SetTheory.Set.instSingleton : Singleton Object Set where
  singleton := singleton

-- Now we can use the `{x}` notation for a single element `Set`.
example (x: Object) : {x} = SetTheory.singleton x := rfl

Axiom 3.3(a) (singleton). Note: in some applications one may have to explicitly cast {a} to Set due to Mathlib's existing set theory notation.

@[simp]
theorem SetTheory.Set.mem_singleton (x a:Object) : x ∈ ({a}:Set) ↔ x = a := singleton_axiom x a

instance SetTheory.Set.instUnion : Union Set where
  union := union_pair

-- Now we can use the `X ∪ Y` notation for a union of two `Set`s.
example (X Y: Set) : X ∪ Y = SetTheory.union_pair X Y := rfl

Axiom 3.4 (Pairwise union)

@[simp]
theorem SetTheory.Set.mem_union (x:Object) (X Y:Set) : x ∈ (X ∪ Y) ↔ (x ∈ X ∨ x ∈ Y) :=
  union_pair_axiom X Y x

instance SetTheory.Set.instInsert : Insert Object Set where
  insert x X := {x} ∪ X

@[simp]
theorem SetTheory.Set.mem_insert (a b: Object) (X: Set) : a ∈ insert b X ↔ a = b ∨ a ∈ X := byinst✝:SetTheorya:Objectb:ObjectX:Set⊢ a ∈ insert b X ↔ a = b ∨ a ∈ X
  simp [instInsert]All goals completed! 🐙

Axiom 3.3(b) (pair). Note: in some applications one may have to cast {a,b} to Set.

theorem SetTheory.Set.pair_eq (a b:Object) : ({a,b}:Set) = {a} ∪ {b} := byinst✝:SetTheorya:Objectb:Object⊢ {a, b} = {a} ∪ {b} rflAll goals completed! 🐙

Axiom 3.3(b) (pair). Note: in some applications one may have to cast {a,b} to Set.

@[simp]
theorem SetTheory.Set.mem_pair (x a b:Object) : x ∈ ({a,b}:Set) ↔ (x = a ∨ x = b) := byinst✝:SetTheoryx:Objecta:Objectb:Object⊢ x ∈ {a, b} ↔ x = a ∨ x = b
  simp [pair_eq, mem_union, mem_singleton]All goals completed! 🐙

@[simp]
theorem SetTheory.Set.mem_triple (x a b c:Object) : x ∈ ({a,b,c}:Set) ↔ (x = a ∨ x = b ∨ x = c) := byinst✝:SetTheoryx:Objecta:Objectb:Objectc:Object⊢ x ∈ {a, b, c} ↔ x = a ∨ x = b ∨ x = c
  simp [Insert.insert, mem_union, mem_singleton]All goals completed! 🐙

Remark 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.singleton_uniq (a:Object) : ∃! (X:Set), ∀ x, x ∈ X ↔ x = a := byinst✝:SetTheorya:Object⊢ ∃! X, ∀ (x : Object), x ∈ X ↔ x = a sorryAll goals completed! 🐙

Remark 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.pair_uniq (a b:Object) : ∃! (X:Set), ∀ x, x ∈ X ↔ x = a ∨ x = b := byinst✝:SetTheorya:Objectb:Object⊢ ∃! X, ∀ (x : Object), x ∈ X ↔ x = a ∨ x = b sorryAll goals completed! 🐙

Remark 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.pair_comm (a b:Object) : ({a,b}:Set) = {b,a} := byinst✝:SetTheorya:Objectb:Object⊢ {a, b} = {b, a} sorryAll goals completed! 🐙

Remark 3.1.9

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.pair_self (a:Object) : ({a,a}:Set) = {a} := byinst✝:SetTheorya:Object⊢ {a, a} = {a}
  sorryAll goals completed! 🐙

Exercise 3.1.1

theorem declaration uses 'sorry'SetTheory.Set.pair_eq_pair {a b c d:Object} (h: ({a,b}:Set) = {c,d}) :
    a = c ∧ b = d ∨ a = d ∧ b = c := byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecth:{a, b} = {c, d}⊢ a = c ∧ b = d ∨ a = d ∧ b = c
  sorryAll goals completed! 🐙

abbrev SetTheory.Set.empty : Set := ∅abbrev SetTheory.Set.singleton_empty : Set := {(empty: Object)}abbrev SetTheory.Set.pair_empty : Set := {(empty: Object), (singleton_empty: Object)}

Exercise 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.emptyset_neq_singleton : empty ≠ singleton_empty := byinst✝:SetTheory⊢ empty ≠ singleton_empty
  sorryAll goals completed! 🐙

Exercise 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.emptyset_neq_pair : empty ≠ pair_empty := byinst✝:SetTheory⊢ empty ≠ pair_empty sorryAll goals completed! 🐙

Exercise 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.singleton_empty_neq_pair : singleton_empty ≠ pair_empty := byinst✝:SetTheory⊢ singleton_empty ≠ pair_empty
  sorryAll goals completed! 🐙

Remark 3.1.11. (These results can be proven either by a direct rewrite, or by using extensionality.)

theorem declaration uses 'sorry'SetTheory.Set.union_congr_left (A A' B:Set) (h: A = A') : A ∪ B = A' ∪ B := byinst✝:SetTheoryA:SetA':SetB:Seth:A = A'⊢ A ∪ B = A' ∪ B sorryAll goals completed! 🐙

Remark 3.1.11. (These results can be proven either by a direct rewrite, or by using extensionality.)

theorem declaration uses 'sorry'SetTheory.Set.union_congr_right (A B B':Set) (h: B = B') : A ∪ B = A ∪ B' := byinst✝:SetTheoryA:SetB:SetB':Seth:B = B'⊢ A ∪ B = A ∪ B' sorryAll goals completed! 🐙

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

theorem declaration uses 'sorry'SetTheory.Set.singleton_union_singleton (a b:Object) :
    ({a}:Set) ∪ ({b}:Set) = {a,b} := byinst✝:SetTheorya:Objectb:Object⊢ {a} ∪ {b} = {a, b}
  sorryAll goals completed! 🐙

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

theorem declaration uses 'sorry'SetTheory.Set.union_comm (A B:Set) : A ∪ B = B ∪ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ B = B ∪ A sorryAll goals completed! 🐙

Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3

theorem declaration uses 'sorry'SetTheory.Set.union_assoc (A B C:Set) : (A ∪ B) ∪ C = A ∪ (B ∪ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C)
  -- this proof is written to follow the structure of the original text.
  ext xhinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C ↔ x ∈ A ∪ (B ∪ C)
  constructorh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C → x ∈ A ∪ (B ∪ C)h.mprinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ (B ∪ C) → x ∈ A ∪ B ∪ C
  .h.mpinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C → x ∈ A ∪ (B ∪ C) intro hxh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Objecthx:x ∈ A ∪ B ∪ C⊢ x ∈ A ∪ (B ∪ C); rw [mem_union] at hxh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Objecthx:x ∈ A ∪ B ∨ x ∈ C⊢ x ∈ A ∪ (B ∪ C)
    obtain case1 | case2 := hxh.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∪ B⊢ x ∈ A ∪ (B ∪ C)h.mp.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ C⊢ x ∈ A ∪ (B ∪ C)
    .h.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∪ B⊢ x ∈ A ∪ (B ∪ C) rw [mem_union] at case1h.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∨ x ∈ B⊢ x ∈ A ∪ (B ∪ C)
      obtain case1a | case1b := case1h.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∪ (B ∪ C)h.mp.inl.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ B⊢ x ∈ A ∪ (B ∪ C)
      .h.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∪ (B ∪ C) rw [mem_union]h.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙
      have : x ∈ B ∪ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C) rw [mem_union]inst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ B⊢ x ∈ B ∨ x ∈ C; tautoAll goals completed! 🐙
      rw [mem_union]h.mp.inl.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ Bthis:_fvar.11059 ∈ _fvar.11031 ∪ _fvar.11032 := ?_mvar.11638⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙
    have : x ∈ B ∪ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C) rw [mem_union]inst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ C⊢ x ∈ B ∨ x ∈ C; tautoAll goals completed! 🐙
    rw [mem_union]h.mp.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ Cthis:_fvar.11059 ∈ _fvar.11031 ∪ _fvar.11032 := ?_mvar.12309⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙
  sorryAll goals completed! 🐙

Proposition 3.1.27(c)

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.union_self (A:Set) : A ∪ A = A := byinst✝:SetTheoryA:Set⊢ A ∪ A = A
  sorryAll goals completed! 🐙

Proposition 3.1.27(a)

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.union_empty (A:Set) : A ∪ ∅ = A := byinst✝:SetTheoryA:Set⊢ A ∪ ∅ = A
  sorryAll goals completed! 🐙

Proposition 3.1.27(a)

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.empty_union (A:Set) : ∅ ∪ A = A := byinst✝:SetTheoryA:Set⊢ ∅ ∪ A = A
  sorryAll goals completed! 🐙

theorem SetTheory.Set.triple_eq (a b c:Object) : {a,b,c} = ({a}:Set) ∪ {b,c} := byinst✝:SetTheorya:Objectb:Objectc:Object⊢ {a, b, c} = {a} ∪ {b, c}
  rflAll goals completed! 🐙

Example 3.1.10

theorem SetTheory.Set.pair_union_pair (a b c:Object) :
    ({a,b}:Set) ∪ {b,c} = {a,b,c} := byinst✝:SetTheorya:Objectb:Objectc:Object⊢ {a, b} ∪ {b, c} = {a, b, c}
  exthinst✝:SetTheorya:Objectb:Objectc:Objectx✝:Object⊢ x✝ ∈ {a, b} ∪ {b, c} ↔ x✝ ∈ {a, b, c}; simp only [mem_union, mem_pair, mem_triple]hinst✝:SetTheorya:Objectb:Objectc:Objectx✝:Object⊢ (x✝ = a ∨ x✝ = b) ∨ x✝ = b ∨ x✝ = c ↔ x✝ = a ∨ x✝ = b ∨ x✝ = c; tautoAll goals completed! 🐙

Definition 3.1.14.

instance SetTheory.Set.instSubset : HasSubset Set where
  Subset X Y := ∀ x, x ∈ X → x ∈ Y

-- Now we can use `⊆` for a subset relationship between two `Set`s.
example (X Y: Set) : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y := byinst✝:SetTheoryX:SetY:Set⊢ X ⊆ Y ↔ ∀ x ∈ X, x ∈ Y rflAll goals completed! 🐙

Definition 3.1.14. Note that the strict subset operation in Mathlib is denoted rather than .

instance SetTheory.Set.instSSubset : HasSSubset Set where
  SSubset X Y := X ⊆ Y ∧ X ≠ Y

-- Now we can use `⊂` for a strict subset relationship between two `Set`s.
example (X Y: Set) : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y := byinst✝:SetTheoryX:SetY:Set⊢ X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y rflAll goals completed! 🐙

Definition 3.1.14.

theorem SetTheory.Set.subset_def (X Y:Set) : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y := byinst✝:SetTheoryX:SetY:Set⊢ X ⊆ Y ↔ ∀ x ∈ X, x ∈ Y rflAll goals completed! 🐙

Definition 3.1.14. Note that the strict subset operation in Mathlib is denoted rather than .

theorem SetTheory.Set.ssubset_def (X Y:Set) : X ⊂ Y ↔ (X ⊆ Y ∧ X ≠ Y) := byinst✝:SetTheoryX:SetY:Set⊢ X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y rflAll goals completed! 🐙

Remark 3.1.15

theorem declaration uses 'sorry'SetTheory.Set.subset_congr_left {A A' B:Set} (hAA':A = A') (hAB: A ⊆ B) : A' ⊆ B := byinst✝:SetTheoryA:SetA':SetB:SethAA':A = A'hAB:A ⊆ B⊢ A' ⊆ B sorryAll goals completed! 🐙

Examples 3.1.16

@[simp, refl]
theorem declaration uses 'sorry'SetTheory.Set.subset_self (A:Set) : A ⊆ A := byinst✝:SetTheoryA:Set⊢ A ⊆ A sorryAll goals completed! 🐙

Examples 3.1.16

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.empty_subset (A:Set) : ∅ ⊆ A := byinst✝:SetTheoryA:Set⊢ ∅ ⊆ A sorryAll goals completed! 🐙

Proposition 3.1.17 (Partial ordering by set inclusion)

theorem SetTheory.Set.subset_trans {A B C:Set} (hAB:A ⊆ B) (hBC:B ⊆ C) : A ⊆ C := byinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ C⊢ A ⊆ C
  -- This proof is written to follow the structure of the original text.
  rw [subset_def]inst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ C⊢ ∀ x ∈ A, x ∈ C
  intro x hxinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ Cx:Objecthx:x ∈ A⊢ x ∈ C
  rw [subset_def] at hABinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ A⊢ x ∈ C
  apply hAB x at hxinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ B⊢ x ∈ C
  apply hBC x at hxinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ C⊢ x ∈ C
  assumptionAll goals completed! 🐙

Proposition 3.1.17 (Partial ordering by set inclusion)

theorem declaration uses 'sorry'SetTheory.Set.subset_antisymm (A B:Set) (hAB:A ⊆ B) (hBA:B ⊆ A) : A = B := byinst✝:SetTheoryA:SetB:SethAB:A ⊆ BhBA:B ⊆ A⊢ A = B
  sorryAll goals completed! 🐙

Proposition 3.1.17 (Partial ordering by set inclusion)

theorem declaration uses 'sorry'SetTheory.Set.ssubset_trans (A B C:Set) (hAB:A ⊂ B) (hBC:B ⊂ C) : A ⊂ C := byinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊂ BhBC:B ⊂ C⊢ A ⊂ C
  sorryAll goals completed! 🐙

This defines the subtype Unknown identifier `A.toSubtype`A.toSubtype for any . Note that Unknown identifier `A.toSubtype`A.toSubtype gives you a type, similar to how Chapter3.SetTheory.Object.{u, v} [self : SetTheory] : Type vObject or Chapter3.SetTheory.Set.{u, v} [self : SetTheory] : Type uSet are types. A value Unknown identifier `x'`x' of type Unknown identifier `A.toSubtype`A.toSubtype combines some with a proof that .

To produce an element Unknown identifier `x'`x' of this subtype, use Invalid `⟨...⟩` notation: The expected type of this term could not be determined⟨ x, hx ⟩, where and . The object Unknown identifier `x`x associated to a subtype element Unknown identifier `x'`x' is recovered as Unknown identifier `x'.val`x'.val, and the property Unknown identifier `hx`hx that Unknown identifier `x`x belongs to Unknown identifier `A`A is recovered as Unknown identifier `x'.property`x'.property.

abbrev SetTheory.Set.toSubtype (A:Set) := Subtype (fun x ↦ x ∈ A)

example (A: Set) (x: Object) (hx: x ∈ A) : A.toSubtype := ⟨x, hx⟩example (A: Set) (x': A.toSubtype) : Object := x'.valexample (A: Set) (x': A.toSubtype) : x'.val ∈ A := x'.property

-- In practice, a subtype lets us carry an object with a membership proof as a single value.
-- Compare these two proofs. They are equivalent, but the latter packs `x` and `hx` into `x'`.
example (A B: Set) (x: Object) (hx: x ∈ A) : x ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A ∨ x ∈ B; lefthinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A; exact hxAll goals completed! 🐙

example (A B: Set) (x': A.toSubtype) : x'.val ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∨ ↑x' ∈ B; lefthinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A; exact x'.propertyAll goals completed! 🐙

instance : CoeSort (Set) (Type v) where
  coe A := A.toSubtype

-- Now instead of writing `x': A.toSubtype`, we can just write `x': A`.
-- Compare these three proofs. They are equivalent, but the last one reads most concisely.
example (A B: Set) (x: Object) (hx: x ∈ A) : x ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A ∨ x ∈ B; lefthinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A; exact hxAll goals completed! 🐙

example (A B: Set) (x': A.toSubtype) : x'.val ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∨ ↑x' ∈ B; lefthinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A; exact x'.propertyAll goals completed! 🐙

example (A B: Set) (x': A) : x'.val ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∨ ↑x' ∈ B; lefthinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A; exact x'.propertyAll goals completed! 🐙

Elements of a set (implicitly coerced to a subtype) are also elements of the set (with respect to the membership operation of the set theory).

lemma SetTheory.Set.subtype_property (A:Set) (x:A) : x.val ∈ A := x.property

lemma SetTheory.Set.subtype_coe (A:Set) (x:A) : x.val = x := rfllemma SetTheory.Set.coe_inj (A:Set) (x y:A) : x.val = y.val ↔ x = y := Subtype.coe_inj

If one has a proof Unknown identifier `hx`hx of Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `A`A, then Unknown identifier `A.subtype_mk`A.subtype_mk hx will then make the element of Unknown identifier `A`A (viewed as a subtype) corresponding to Unknown identifier `x`x.

def SetTheory.Set.subtype_mk (A:Set) {x:Object} (hx:x ∈ A) : A := ⟨ x, hx ⟩

@[simp]
lemma SetTheory.Set.subtype_mk_coe {A:Set} {x:Object} (hx:x ∈ A) : A.subtype_mk hx = x := byinst✝:SetTheoryA:Setx:Objecthx:x ∈ A⊢ ↑(A.subtype_mk hx) = x rflAll goals completed! 🐙

abbrev SetTheory.Set.specify (A:Set) (P: A → Prop) : Set := SetTheory.specify A P

Axiom 3.6 (axiom of specification)

theorem SetTheory.Set.specification_axiom {A:Set} {P: A → Prop} {x:Object} (h: x ∈ A.specify P) :
    x ∈ A :=
  (SetTheory.specification_axiom A P).1 x h

Axiom 3.6 (axiom of specification)

theorem SetTheory.Set.specification_axiom' {A:Set} (P: A → Prop) (x:A) :
    x.val ∈ A.specify P ↔ P x :=
  (SetTheory.specification_axiom A P).2 x

Axiom 3.6 (axiom of specification)

@[simp]
theorem SetTheory.Set.specification_axiom'' {A:Set} (P: A → Prop) (x:Object) :
    x ∈ A.specify P ↔ ∃ h:x ∈ A, P ⟨ x, h ⟩ := byinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Object⊢ x ∈ A.specify P ↔ ∃ (h : x ∈ A), P ⟨x, h⟩
  constructormpinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Object⊢ x ∈ A.specify P → ∃ (h : x ∈ A), P ⟨x, h⟩mprinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Object⊢ (∃ (h : x ∈ A), P ⟨x, h⟩) → x ∈ A.specify P
  .mpinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Object⊢ x ∈ A.specify P → ∃ (h : x ∈ A), P ⟨x, h⟩ intro hmpinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ A.specify P⊢ ∃ (h : x ∈ A), P ⟨x, h⟩; use specification_axiom hhinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ A.specify P⊢ P ⟨x, ⋯⟩
    simp [←specification_axiom' P, h]All goals completed! 🐙
  intro ⟨ h, hP ⟩mprinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ AhP:P ⟨x, h⟩⊢ x ∈ A.specify P
  simpa [←specification_axiom' P] using hPAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.specify_subset {A:Set} (P: A → Prop) : A.specify P ⊆ A := byinst✝:SetTheoryA:SetP:A.toSubtype → Prop⊢ A.specify P ⊆ A sorryAll goals completed! 🐙

This exercise may require some understanding of how subtypes are implemented in Lean.

theorem declaration uses 'sorry'SetTheory.Set.specify_congr {A A':Set} (hAA':A = A') {P: A → Prop} {P': A' → Prop}
  (hPP': (x:Object) → (h:x ∈ A) → (h':x ∈ A') → P ⟨ x, h⟩ ↔ P' ⟨ x, h'⟩ ) :
    A.specify P = A'.specify P' := byinst✝:SetTheoryA:SetA':SethAA':A = A'P:A.toSubtype → PropP':A'.toSubtype → ProphPP':∀ (x : Object) (h : x ∈ A) (h' : x ∈ A'), P ⟨x, h⟩ ↔ P' ⟨x, h'⟩⊢ A.specify P = A'.specify P' sorryAll goals completed! 🐙

instance SetTheory.Set.instIntersection : Inter Set where
  inter X Y := X.specify (fun x ↦ x.val ∈ Y)

-- Now we can use the `X ∩ Y` notation for an intersection of two `Set`s.
example (X Y: Set) : X ∩ Y = X.specify (fun x ↦ x.val ∈ Y) := rfl

Definition 3.1.22 (Intersections)

@[simp]
theorem SetTheory.Set.mem_inter (x:Object) (X Y:Set) : x ∈ (X ∩ Y) ↔ (x ∈ X ∧ x ∈ Y) := byinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y
  constructormpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y → x ∈ X ∧ x ∈ Ymprinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∧ x ∈ Y → x ∈ X ∩ Y
  .mpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y → x ∈ X ∧ x ∈ Y intro hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Y⊢ x ∈ X ∧ x ∈ Y; have h' := specification_axiom hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Yh':?_mvar.29648 := Chapter3.SetTheory.Set.specification_axiom _fvar.29644⊢ x ∈ X ∧ x ∈ Y; simp [h']mpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Yh':?_mvar.29648 := Chapter3.SetTheory.Set.specification_axiom _fvar.29644⊢ x ∈ Y
    exact (specification_axiom' _ ⟨ x, h' ⟩).mp hAll goals completed! 🐙
  intro ⟨ hX, hY ⟩mprinst✝:SetTheoryx:ObjectX:SetY:SethX:x ∈ XhY:x ∈ Y⊢ x ∈ X ∩ Y; exact (specification_axiom' (fun x ↦ x.val ∈ Y) ⟨ x,hX⟩).mpr hYAll goals completed! 🐙

instance SetTheory.Set.instSDiff : SDiff Set where
  sdiff X Y := X.specify (fun x ↦ x.val ∉ Y)

-- Now we can use the `X \ Y` notation for a difference of two `Set`s.
example (X Y: Set) : X \ Y = X.specify (fun x ↦ x.val ∉ Y) := rfl

Definition 3.1.26 (Difference sets)

@[simp]
theorem SetTheory.Set.mem_sdiff (x:Object) (X Y:Set) : x ∈ (X \ Y) ↔ (x ∈ X ∧ x ∉ Y) := byinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y ↔ x ∈ X ∧ x ∉ Y
  constructormpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y → x ∈ X ∧ x ∉ Ymprinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∧ x ∉ Y → x ∈ X \ Y
  .mpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y → x ∈ X ∧ x ∉ Y intro hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Y⊢ x ∈ X ∧ x ∉ Y; have h' := specification_axiom hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Yh':?_mvar.30370 := Chapter3.SetTheory.Set.specification_axiom _fvar.30366⊢ x ∈ X ∧ x ∉ Y; simp [h']mpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Yh':?_mvar.30370 := Chapter3.SetTheory.Set.specification_axiom _fvar.30366⊢ x ∉ Y
    exact (specification_axiom' _ ⟨ x, h' ⟩ ).mp hAll goals completed! 🐙
  intro ⟨ hX, hY ⟩mprinst✝:SetTheoryx:ObjectX:SetY:SethX:x ∈ XhY:x ∉ Y⊢ x ∈ X \ Y; exact (specification_axiom' (fun x ↦ x.val ∉ Y) ⟨ x, hX⟩ ).mpr hYAll goals completed! 🐙

Proposition 3.1.27(d) / Exercise 3.1.6

theorem declaration uses 'sorry'SetTheory.Set.inter_comm (A B:Set) : A ∩ B = B ∩ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B = B ∩ A sorryAll goals completed! 🐙

Proposition 3.1.27(b)

theorem declaration uses 'sorry'SetTheory.Set.subset_union {A X: Set} (hAX: A ⊆ X) : A ∪ X = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ A ∪ X = X sorryAll goals completed! 🐙

Proposition 3.1.27(b)

theorem declaration uses 'sorry'SetTheory.Set.union_subset {A X: Set} (hAX: A ⊆ X) : X ∪ A = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ X ∪ A = X sorryAll goals completed! 🐙

Proposition 3.1.27(c)

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.inter_self (A:Set) : A ∩ A = A := byinst✝:SetTheoryA:Set⊢ A ∩ A = A
  sorryAll goals completed! 🐙

Proposition 3.1.27(e)

theorem declaration uses 'sorry'SetTheory.Set.inter_assoc (A B C:Set) : (A ∩ B) ∩ C = A ∩ (B ∩ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∩ B ∩ C = A ∩ (B ∩ C) sorryAll goals completed! 🐙

Proposition 3.1.27(f)

theorem  declaration uses 'sorry'SetTheory.Set.inter_union_distrib_left (A B C:Set) :
    A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∩ (B ∪ C) = A ∩ B ∪ A ∩ C
  sorryAll goals completed! 🐙

Proposition 3.1.27(f)

theorem  declaration uses 'sorry'SetTheory.Set.union_inter_distrib_left (A B C:Set) :
    A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∩ C = (A ∪ B) ∩ (A ∪ C)
  sorryAll goals completed! 🐙

Proposition 3.1.27(f)

theorem declaration uses 'sorry'SetTheory.Set.union_compl {A X:Set} (hAX: A ⊆ X) : A ∪ (X \ A) = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ A ∪ X \ A = X sorryAll goals completed! 🐙

Proposition 3.1.27(f)

theorem declaration uses 'sorry'SetTheory.Set.inter_compl {A X:Set} : A ∩ (X \ A) = ∅ := byinst✝:SetTheoryA:SetX:Set⊢ A ∩ (X \ A) = ∅ sorryAll goals completed! 🐙

Proposition 3.1.27(g)

theorem declaration uses 'sorry'SetTheory.Set.compl_union {A B X:Set} : X \ (A ∪ B) = (X \ A) ∩ (X \ B) := byinst✝:SetTheoryA:SetB:SetX:Set⊢ X \ (A ∪ B) = X \ A ∩ (X \ B) sorryAll goals completed! 🐙

Proposition 3.1.27(g)

theorem declaration uses 'sorry'SetTheory.Set.compl_inter {A B X:Set} : X \ (A ∩ B) = (X \ A) ∪ (X \ B) := byinst✝:SetTheoryA:SetB:SetX:Set⊢ X \ (A ∩ B) = X \ A ∪ X \ B sorryAll goals completed! 🐙

Not from textbook: sets form a distributive lattice.

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.instDistribLattice : DistribLattice Set where
  le := (·⊆ ·)
  le_refl := subset_self
  le_trans := fun _ _ _ ↦ subset_trans
  le_antisymm := subset_antisymm
  inf := (·∩ ·)
  sup := (·∪ ·)
  le_sup_left := byinst✝:SetTheory⊢ ∀ (a b : Set), a ⊆ a ∪ b sorryAll goals completed! 🐙
  le_sup_right := byinst✝:SetTheory⊢ ∀ (a b : Set), b ⊆ a ∪ b sorryAll goals completed! 🐙
  sup_le := byinst✝:SetTheory⊢ ∀ (a b c : Set), a ⊆ c → b ⊆ c → a ∪ b ⊆ c sorryAll goals completed! 🐙
  inf_le_left := byinst✝:SetTheory⊢ ∀ (a b : Set), a ∩ b ⊆ a sorryAll goals completed! 🐙
  inf_le_right := byinst✝:SetTheory⊢ ∀ (a b : Set), a ∩ b ⊆ b sorryAll goals completed! 🐙
  le_inf := byinst✝:SetTheory⊢ ∀ (a b c : Set), a ⊆ b → a ⊆ c → a ⊆ b ∩ c sorryAll goals completed! 🐙
  le_sup_inf := byinst✝:SetTheory⊢ ∀ (x y z : Set), (x ⊔ y) ⊓ (x ⊔ z) ⊆ x ⊔ y ⊓ z
    intro X Y Zinst✝:SetTheoryX:SetY:SetZ:Set⊢ (X ⊔ Y) ⊓ (X ⊔ Z) ⊆ X ⊔ Y ⊓ Z; change (X ∪ Y) ∩ (X ∪ Z) ⊆ X ∪ (Y ∩ Z)inst✝:SetTheoryX:SetY:SetZ:Set⊢ (X ∪ Y) ∩ (X ∪ Z) ⊆ X ∪ Y ∩ Z
    rw [←union_inter_distrib_left]All goals completed! 🐙

Sets have a minimal element.

instance SetTheory.Set.instOrderBot : OrderBot Set where
  bot := ∅
  bot_le := empty_subset

-- Now we've defined `A ≤ B` to mean `A ⊆ B`, and set `⊥` to `∅`.
-- This makes the `Disjoint` definition from Mathlib work with our `Set`.
example (A B: Set) : (A ≤ B) ↔ (A ⊆ B) := byinst✝:SetTheoryA:SetB:Set⊢ A ≤ B ↔ A ⊆ B rflAll goals completed! 🐙

example : ⊥ = (∅: Set) := byinst✝:SetTheory⊢ ⊥ = ∅ rflAll goals completed! 🐙example (A B: Set) : Prop := Disjoint A B

Definition of disjointness (using the previous instances)

theorem SetTheory.Set.disjoint_iff (A B:Set) : Disjoint A B ↔ A ∩ B = ∅ := byinst✝:SetTheoryA:SetB:Set⊢ Disjoint A B ↔ A ∩ B = ∅
  convert _root_.disjoint_iffAll goals completed! 🐙

abbrev SetTheory.Set.replace (A:Set) {P: A → Object → Prop}
  (hP : ∀ x y y', P x y ∧ P x y' → y = y') : Set := SetTheory.replace A P hP

Axiom 3.7 (Axiom of replacement)

@[simp]
theorem SetTheory.Set.replacement_axiom {A:Set} {P: A → Object → Prop}
  (hP: ∀ x y y', P x y ∧ P x y' → y = y') (y:Object) :
    y ∈ A.replace hP ↔ ∃ x, P x y := SetTheory.replacement_axiom A P hP y

abbrev Nat := SetTheory.nat

-- Going forward, we'll use `Nat` as a type.
-- However, notice we've set `Nat` to `SetTheory.nat` which is a `Set` and not a type.
-- The only reason we can write `x: Nat` is because we've previously defined a `CoeSort`
-- coercion that lets us write `x: A` (when `A` is a `Set`) as a shortcut for `x: A.toSubtype`.
-- This is why, whenever you see `x: Nat`, you're really looking at `x: Nat.toSubtype`.
example (x: Nat) : Nat.toSubtype := x

example (x: Nat) : Object := x.valexample (x: Nat) : (x.val ∈ Nat) := x.propertyexample (o: Object) (ho: o ∈ Nat) : Nat := ⟨o, ho⟩

Axiom 3.8 (Axiom of infinity)

def SetTheory.Set.nat_equiv : ℕ ≃ Nat := SetTheory.nat_equiv

-- Below are some API for handling coercions. This may not be the optimal way to set things up.
instance SetTheory.Set.instOfNat {n:ℕ} : OfNat Nat n where
  ofNat := nat_equiv n

-- Now we can define `Nat` with a natural literal.
example : Nat := 5

example : (5 : Nat).val ∈ Nat := (5 : Nat).property

instance SetTheory.Set.instNatCast : NatCast Nat where
  natCast n := nat_equiv n

-- Now we can turn `ℕ` into `Nat`.
example (n : ℕ) : Nat := n

example (n : ℕ) : (n : Nat).val ∈ Nat := (n : Nat).property

instance SetTheory.Set.toNat : Coe Nat ℕ where
  coe n := nat_equiv.symm n

-- Now we can turn `Nat` into `ℕ`.
example (n : Nat) : ℕ := n

instance SetTheory.Object.instNatCast : NatCast Object where
  natCast n := (n:Nat).val

-- Now we can turn `ℕ` into an `Object`.
example (n: ℕ) : Object := n

example (n: ℕ) : Set := {(n: Object)}

instance SetTheory.Object.instOfNat {n:ℕ} : OfNat Object n where
  ofNat := ((n:Nat):Object)

-- Now we can define `Object` with a natural literal.
example : Object := 1

example : Set := {1, 2, 3}

@[simp]
lemma SetTheory.Object.ofnat_eq {n:ℕ} : ((n:Nat):Object) = (n:Object) := rfl

lemma SetTheory.Object.ofnat_eq' {n:ℕ} : (ofNat(n):Object) = (n:Object) := rfl

@[simp]
lemma SetTheory.Object.ofnat_eq'' {n:Nat} : ((n:ℕ):Object) = (n: Object) := byinst✝:SetTheoryn:Nat.toSubtype⊢ ↑(Set.nat_equiv.symm n) = ↑n
  simp [instNatCast, Nat.cast, Set.instNatCast]All goals completed! 🐙

@[simp]
lemma SetTheory.Object.ofnat_eq''' {n:ℕ} {hn} : ((⟨(n:Object), hn⟩: nat): ℕ) = n := byinst✝:SetTheoryn:ℕhn:↑n ∈ nat⊢ Set.nat_equiv.symm ⟨↑n, hn⟩ = n
  simp [instNatCast, Nat.cast, Set.instNatCast]All goals completed! 🐙

lemma SetTheory.Set.nat_coe_eq {n:ℕ} : (n:Nat) = OfNat.ofNat n := rfl

@[simp]
lemma SetTheory.Set.nat_equiv_inj (n m:ℕ) : (n:Nat) = (m:Nat) ↔ n=m  :=
  Equiv.apply_eq_iff_eq nat_equiv

@[simp]
lemma SetTheory.Set.nat_equiv_symm_inj (n m:Nat) : (n:ℕ) = (m:ℕ) ↔ n = m :=
  Equiv.apply_eq_iff_eq nat_equiv.symm

@[simp]
theorem SetTheory.Set.ofNat_inj (n m:ℕ) :
    (ofNat(n) : Nat) = (ofNat(m) : Nat) ↔ ofNat(n) = ofNat(m) := byinst✝:SetTheoryn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m
      convert nat_equiv_inj _ _All goals completed! 🐙

example : (5:Nat) ≠ (3:Nat) := byinst✝:SetTheory⊢ 5 ≠ 3
  simpAll goals completed! 🐙

@[simp]
theorem SetTheory.Set.ofNat_inj' (n m:ℕ) :
    (ofNat(n) : Object) = (ofNat(m) : Object) ↔ ofNat(n) = ofNat(m) := byinst✝:SetTheoryn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m
      simp only [←Object.ofnat_eq, Object.ofnat_eq', Set.coe_inj, Set.nat_equiv_inj]inst✝:SetTheoryn:ℕm:ℕ⊢ n = m ↔ OfNat.ofNat n = OfNat.ofNat m
      rflAll goals completed! 🐙

example : (5:Object) ≠ (3:Object) := byinst✝:SetTheory⊢ 5 ≠ 3
  simpAll goals completed! 🐙

@[simp]
lemma SetTheory.Set.nat_coe_eq_iff {m n : ℕ} : (m:Object) = ofNat(n) ↔ m = n := byinst✝:SetTheorym:ℕn:ℕ⊢ ↑m = OfNat.ofNat n ↔ m = n exact ofNat_inj' m nAll goals completed! 🐙

example (n: ℕ) : (n: Object) = 2 ↔ n = 2 := byinst✝:SetTheoryn:ℕ⊢ ↑n = 2 ↔ n = 2
  simpAll goals completed! 🐙

@[simp]
theorem SetTheory.Object.natCast_inj (n m:ℕ) :
    (n : Object) = (m : Object) ↔ n = m := byinst✝:SetTheoryn:ℕm:ℕ⊢ ↑n = ↑m ↔ n = m
      simp [←ofnat_eq, Subtype.val_inj]All goals completed! 🐙

@[simp]
lemma SetTheory.Set.nat_equiv_coe_of_coe (n:ℕ) : ((n:Nat):ℕ) = n :=
  Equiv.symm_apply_apply nat_equiv n

@[simp]
lemma SetTheory.Set.nat_equiv_coe_of_coe' (n:Nat) : ((n:ℕ):Nat) = n :=
  Equiv.symm_apply_apply nat_equiv.symm n

@[simp]
lemma SetTheory.Set.nat_equiv_coe_of_coe'' (n:ℕ) : ((ofNat(n):Nat):ℕ) = n :=
  nat_equiv_coe_of_coe n

@[simp]
lemma SetTheory.Set.nat_coe_eq_iff' {m: Nat} {n : ℕ} : (m:Object) = (ofNat(n):Object) ↔ (m:ℕ) = ofNat(n) := byinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ ↑m = OfNat.ofNat n ↔ nat_equiv.symm m = OfNat.ofNat n
  constructormpinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ ↑m = OfNat.ofNat n → nat_equiv.symm m = OfNat.ofNat nmprinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ nat_equiv.symm m = OfNat.ofNat n → ↑m = OfNat.ofNat n <;>mpinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ ↑m = OfNat.ofNat n → nat_equiv.symm m = OfNat.ofNat nmprinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ nat_equiv.symm m = OfNat.ofNat n → ↑m = OfNat.ofNat n intro hmprinst✝:SetTheorym:Nat.toSubtypen:ℕh:nat_equiv.symm m = OfNat.ofNat n⊢ ↑m = OfNat.ofNat n <;>mpinst✝:SetTheorym:Nat.toSubtypen:ℕh:↑m = OfNat.ofNat n⊢ nat_equiv.symm m = OfNat.ofNat nmprinst✝:SetTheorym:Nat.toSubtypen:ℕh:nat_equiv.symm m = OfNat.ofNat n⊢ ↑m = OfNat.ofNat n rw [show m = n by aesop]mprinst✝:SetTheorym:Nat.toSubtypen:ℕh:nat_equiv.symm m = OfNat.ofNat n⊢ ↑↑n = OfNat.ofNat n
  apply nat_equiv_coe_of_coemprinst✝:SetTheorym:Nat.toSubtypen:ℕh:nat_equiv.symm m = OfNat.ofNat n⊢ ↑↑n = OfNat.ofNat n; rflAll goals completed! 🐙

Example 3.1.16 (simplified).

example : ({3, 5}:Set) ⊆ {1, 3, 5} := byinst✝:SetTheory⊢ {3, 5} ⊆ {1, 3, 5}
  simp only [subset_def, mem_pair, mem_triple]inst✝:SetTheory⊢ ∀ (x : Object), x = 3 ∨ x = 5 → x = 1 ∨ x = 3 ∨ x = 5; tautoAll goals completed! 🐙

Example 3.1.17 (simplified).

example : ({3, 5}:Set).specify (fun x ↦ x.val ≠ 3) = ({5}:Set) := byinst✝:SetTheory⊢ ({3, 5}.specify fun x => ↑x ≠ 3) = {5}
  exthinst✝:SetTheoryx✝:Object⊢ (x✝ ∈ {3, 5}.specify fun x => ↑x ≠ 3) ↔ x✝ ∈ {5}
  simp only [mem_singleton, specification_axiom'']hinst✝:SetTheoryx✝:Object⊢ (∃ (_ : x✝ ∈ {3, 5}), x✝ ≠ 3) ↔ x✝ = 5
  constructorh.mpinst✝:SetTheoryx✝:Object⊢ (∃ (_ : x✝ ∈ {3, 5}), x✝ ≠ 3) → x✝ = 5h.mprinst✝:SetTheoryx✝:Object⊢ x✝ = 5 → ∃ (_ : x✝ ∈ {3, 5}), x✝ ≠ 3
  ·h.mpinst✝:SetTheoryx✝:Object⊢ (∃ (_ : x✝ ∈ {3, 5}), x✝ ≠ 3) → x✝ = 5 rintro ⟨h1, h2⟩h.mp.introinst✝:SetTheoryx✝:Objecth1:x✝ ∈ {3, 5}h2:x✝ ≠ 3⊢ x✝ = 5; simp only [mem_pair] at h1h.mp.introinst✝:SetTheoryx✝:Objecth2:x✝ ≠ 3h1:x✝ = 3 ∨ x✝ = 5⊢ x✝ = 5; tautoAll goals completed! 🐙
  rintro ⟨rfl⟩h.mpr.reflinst✝:SetTheory⊢ ∃ (_ : 5 ∈ {3, 5}), 5 ≠ 3; norm_numAll goals completed! 🐙

Example 3.1.24

example : ({1, 2, 4}:Set) ∩ {2,3,4} = {2, 4} := byinst✝:SetTheory⊢ {1, 2, 4} ∩ {2, 3, 4} = {2, 4}
  ext xhinst✝:SetTheoryx:Object⊢ x ∈ {1, 2, 4} ∩ {2, 3, 4} ↔ x ∈ {2, 4}
  -- Instead of unfolding repetitive branches by hand like earlier,
  -- you can use the `aesop` tactic which does this automatically.
  aesopAll goals completed! 🐙

Example 3.1.24

example : ({1, 2}:Set) ∩ {3,4} = ∅ := byinst✝:SetTheory⊢ {1, 2} ∩ {3, 4} = ∅
  rw [eq_empty_iff_forall_notMem]inst✝:SetTheory⊢ ∀ (x : Object), x ∉ {1, 2} ∩ {3, 4}
  aesopAll goals completed! 🐙

example : ¬ Disjoint ({1, 2, 3}:Set) {2,3,4} := byinst✝:SetTheory⊢ ¬Disjoint {1, 2, 3} {2, 3, 4}
  rw [disjoint_iff]inst✝:SetTheory⊢ ¬{1, 2, 3} ∩ {2, 3, 4} = ∅
  intro hinst✝:SetTheoryh:{1, 2, 3} ∩ {2, 3, 4} = ∅⊢ False
  change {1, 2, 3} ∩ {2, 3, 4} = ∅ at hinst✝:SetTheoryh:{1, 2, 3} ∩ {2, 3, 4} = ∅⊢ False
  rw [eq_empty_iff_forall_notMem] at hinst✝:SetTheoryh:∀ (x : Object), x ∉ {1, 2, 3} ∩ {2, 3, 4}⊢ False
  aesopAll goals completed! 🐙

declaration uses 'sorry'example : Disjoint (∅:Set) ∅ := byinst✝:SetTheory⊢ Disjoint ∅ ∅ sorryAll goals completed! 🐙

Definition 3.1.26 example

example : ({1, 2, 3, 4}:Set) \ {2,4,6} = {1, 3} := byinst✝:SetTheory⊢ {1, 2, 3, 4} \ {2, 4, 6} = {1, 3}
  apply exthinst✝:SetTheory⊢ ∀ (x : Object), x ∈ {1, 2, 3, 4} \ {2, 4, 6} ↔ x ∈ {1, 3}; aesopAll goals completed! 🐙

Example 3.1.30

declaration uses 'sorry'example : ({3,5,9}:Set).replace (P := fun x y ↦ ∃ (n:ℕ), x.val = n ∧ y = (n+1:ℕ)) (byinst✝:SetTheory⊢ ∀ (x : {3, 5, 9}.toSubtype) (y y' : Object),
  (fun x y => ∃ n, ↑x = ↑n ∧ y = ↑(n + 1)) x y ∧ (fun x y => ∃ n, ↑x = ↑n ∧ y = ↑(n + 1)) x y' → y = y' aesopAll goals completed! 🐙)
  = {4,6,10} := byinst✝:SetTheory⊢ {3, 5, 9}.replace ⋯ = {4, 6, 10} sorryAll goals completed! 🐙

Example 3.1.31

example : ({3,5,9}:Set).replace (P := fun _ y ↦ y=1) (byinst✝:SetTheory⊢ ∀ (x : {3, 5, 9}.toSubtype) (y y' : Object), (fun x y => y = 1) x y ∧ (fun x y => y = 1) x y' → y = y' aesopAll goals completed! 🐙) = {1} := byinst✝:SetTheory⊢ {3, 5, 9}.replace ⋯ = {1}
  exthinst✝:SetTheoryx✝:Object⊢ x✝ ∈ {3, 5, 9}.replace ⋯ ↔ x✝ ∈ {1}; simp only [replacement_axiom]hinst✝:SetTheoryx✝:Object⊢ (∃ x, x✝ = 1) ↔ x✝ ∈ {1}; aesopAll goals completed! 🐙

Exercise 3.1.5. One can use the Unknown identifier `tfae_have`tfae_have and Unknown identifier `tfae_finish`tfae_finish tactics here.

theorem declaration uses 'sorry'SetTheory.Set.subset_tfae (A B:Set) : [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE := byinst✝:SetTheoryA:SetB:Set⊢ [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.inter_subset_left (A B:Set) : A ∩ B ⊆ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B ⊆ A
  sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.inter_subset_right (A B:Set) : A ∩ B ⊆ B := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B ⊆ B
  sorryAll goals completed! 🐙

Exercise 3.1.7

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.subset_inter_iff (A B C:Set) : C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B := byinst✝:SetTheoryA:SetB:SetC:Set⊢ C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B
  sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.subset_union_left (A B:Set) : A ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:Set⊢ A ⊆ A ∪ B
  sorryAll goals completed! 🐙

Exercise 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.subset_union_right (A B:Set) : B ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:Set⊢ B ⊆ A ∪ B
  sorryAll goals completed! 🐙

Exercise 3.1.7

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.union_subset_iff (A B C:Set) : A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C
  sorryAll goals completed! 🐙

Exercise 3.1.8

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.inter_union_cancel (A B:Set) : A ∩ (A ∪ B) = A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ (A ∪ B) = A sorryAll goals completed! 🐙

Exercise 3.1.8

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.union_inter_cancel (A B:Set) : A ∪ (A ∩ B) = A := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ A ∩ B = A sorryAll goals completed! 🐙

Exercise 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.partition_left {A B X:Set} (h_union: A ∪ B = X) (h_inter: A ∩ B = ∅) :
    A = X \ B := byinst✝:SetTheoryA:SetB:SetX:Seth_union:A ∪ B = Xh_inter:A ∩ B = ∅⊢ A = X \ B sorryAll goals completed! 🐙

Exercise 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.partition_right {A B X:Set} (h_union: A ∪ B = X) (h_inter: A ∩ B = ∅) :
    B = X \ A := byinst✝:SetTheoryA:SetB:SetX:Seth_union:A ∪ B = Xh_inter:A ∩ B = ∅⊢ B = X \ A
  sorryAll goals completed! 🐙

Exercise 3.1.10. You may find Function.onFun_apply.{u_1, u_2, u_3} {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : β → β → γ) (g : α → β) (a b : α) : Function.onFun f g a b = f (g a) (g b)Function.onFun_apply and the Unknown identifier `fin_cases`fin_cases tactic useful.

theorem declaration uses 'sorry'SetTheory.Set.pairwise_disjoint (A B:Set) :
    Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A]) := byinst✝:SetTheoryA:SetB:Set⊢ Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A]) sorryAll goals completed! 🐙

Exercise 3.1.10

theorem declaration uses 'sorry'SetTheory.Set.union_eq_partition (A B:Set) : A ∪ B = (A \ B) ∪ (A ∩ B) ∪ (B \ A) := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ B = A \ B ∪ A ∩ B ∪ B \ A
  sorryAll goals completed! 🐙

Exercise 3.1.11. The challenge is to prove this without using Unknown constant `specify`Set.specify, Unknown constant `specification_axiom`Set.specification_axiom, Unknown constant `specification_axiom'`Set.specification_axiom', or anything built from them (like differences and intersections).

theorem declaration uses 'sorry'SetTheory.Set.specification_from_replacement {A:Set} {P: A → Prop} :
    ∃ B, B ⊆ A ∧ ∀ x, x.val ∈ B ↔ P x := byinst✝:SetTheoryA:SetP:A.toSubtype → Prop⊢ ∃ B ⊆ A, ∀ (x : A.toSubtype), ↑x ∈ B ↔ P x sorryAll goals completed! 🐙

Exercise 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_union_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) :
    A' ∪ B' ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:SetA':SetB':SethA'A:A' ⊆ AhB'B:B' ⊆ B⊢ A' ∪ B' ⊆ A ∪ B sorryAll goals completed! 🐙

Exercise 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_inter_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) :
    A' ∩ B' ⊆ A ∩ B := byinst✝:SetTheoryA:SetB:SetA':SetB':SethA'A:A' ⊆ AhB'B:B' ⊆ B⊢ A' ∩ B' ⊆ A ∩ B sorryAll goals completed! 🐙

Exercise 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_diff_subset_counter :
    ∃ (A B A' B':Set), (A' ⊆ A) ∧ (B' ⊆ B) ∧ ¬ (A' \ B') ⊆ (A \ B) := byinst✝:SetTheory⊢ ∃ A B A' B', A' ⊆ A ∧ B' ⊆ B ∧ ¬A' \ B' ⊆ A \ B sorryAll goals completed! 🐙

/-
  Final part of Exercise 3.1.12: state and prove a reasonable substitute positive result for the
  above theorem that involves set differences.
-/

Exercise 3.1.13

theorem declaration uses 'sorry'SetTheory.Set.singleton_iff (A:Set) (hA: A ≠ ∅) : (¬∃ B ⊂ A, B ≠ ∅) ↔ ∃ x, A = {x} := byinst✝:SetTheoryA:SethA:A ≠ ∅⊢ (¬∃ B ⊂ A, B ≠ ∅) ↔ ∃ x, A = {x} sorryAll goals completed! 🐙

/-
  Now we introduce connections between this notion of a set, and Mathlib's notion.
  The exercise below will acquiant you with the API for Mathlib's sets.
-/

instance SetTheory.Set.inst_coe_set : Coe Set (_root_.Set Object) where
  coe X := { x | x ∈ X }

-- Now we can convert our `Set` into a Mathlib `_root_.Set`.
-- Notice that Mathlib sets are parameterized by the element type, in our case `Object`.
example (X: Set) : _root_.Set Object := X

Injectivity of the coercion. Note however that we do NOT assert that the coercion is surjective (and indeed Russell's paradox prevents this)

@[simp]
theorem SetTheory.Set.coe_inj' (X Y:Set) :
    (X : _root_.Set Object) = (Y : _root_.Set Object) ↔ X = Y := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} = {x | x ∈ Y} ↔ X = Y
  constructormpinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} = {x | x ∈ Y} → X = Ymprinst✝:SetTheoryX:SetY:Set⊢ X = Y → {x | x ∈ X} = {x | x ∈ Y}
  .mpinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} = {x | x ∈ Y} → X = Y intro hmpinst✝:SetTheoryX:SetY:Seth:{x | x ∈ X} = {x | x ∈ Y}⊢ X = Y; apply extmp.hinst✝:SetTheoryX:SetY:Seth:{x | x ∈ X} = {x | x ∈ Y}⊢ ∀ (x : Object), x ∈ X ↔ x ∈ Y; intro xmp.hinst✝:SetTheoryX:SetY:Seth:{x | x ∈ X} = {x | x ∈ Y}x:Object⊢ x ∈ X ↔ x ∈ Y
    replace h := congr(x ∈ $h)mp.hinst✝:SetTheoryX:SetY:Setx:Objecth:?_mvar.127178 := id (congrArg (fun x => _fvar.127174 ∈ x) _fvar.127156)⊢ x ∈ X ↔ x ∈ Y; simpa using hAll goals completed! 🐙
  rintro rflmprinst✝:SetTheoryX:Set⊢ {x | x ∈ X} = {x | x ∈ X}; rflAll goals completed! 🐙

Compatibility of the membership operation ∈

theorem SetTheory.Set.mem_coe (X:Set) (x:Object) : x ∈ (X : _root_.Set Object) ↔ x ∈ X := byinst✝:SetTheoryX:Setx:Object⊢ x ∈ {x | x ∈ X} ↔ x ∈ X
  simpAll goals completed! 🐙

Compatibility of the emptyset

theorem declaration uses 'sorry'SetTheory.Set.coe_empty : ((∅:Set) : _root_.Set Object) = ∅ := byinst✝:SetTheory⊢ {x | x ∈ ∅} = ∅ sorryAll goals completed! 🐙

Compatibility of subset

theorem declaration uses 'sorry'SetTheory.Set.coe_subset (X Y:Set) :
    (X : _root_.Set Object) ⊆ (Y : _root_.Set Object) ↔ X ⊆ Y := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} ⊆ {x | x ∈ Y} ↔ X ⊆ Y sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.coe_ssubset (X Y:Set) :
    (X : _root_.Set Object) ⊂ (Y : _root_.Set Object) ↔ X ⊂ Y := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} ⊂ {x | x ∈ Y} ↔ X ⊂ Y sorryAll goals completed! 🐙

Compatibility of singleton

theorem declaration uses 'sorry'SetTheory.Set.coe_singleton (x: Object) : ({x} : _root_.Set Object) = {x} := byinst✝:SetTheoryx:Object⊢ {x} = {x} sorryAll goals completed! 🐙

Compatibility of union

theorem declaration uses 'sorry'SetTheory.Set.coe_union (X Y: Set) :
    (X ∪ Y : _root_.Set Object) = (X : _root_.Set Object) ∪ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} ∪ {x | x ∈ Y} = {x | x ∈ X} ∪ {x | x ∈ Y} sorryAll goals completed! 🐙

Compatibility of pair

theorem declaration uses 'sorry'SetTheory.Set.coe_pair (x y: Object) : ({x, y} : _root_.Set Object) = {x, y} := byinst✝:SetTheoryx:Objecty:Object⊢ {x, y} = {x, y} sorryAll goals completed! 🐙

Compatibility of subtype

theorem declaration uses 'sorry'SetTheory.Set.coe_subtype (X: Set) :  (X : _root_.Set Object) = X.toSubtype := byinst✝:SetTheoryX:Set⊢ ↑{x | x ∈ X} = X.toSubtype sorryAll goals completed! 🐙

Compatibility of intersection

theorem declaration uses 'sorry'SetTheory.Set.coe_intersection (X Y: Set) :
    (X ∩ Y : _root_.Set Object) = (X : _root_.Set Object) ∩ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} ∩ {x | x ∈ Y} = {x | x ∈ X} ∩ {x | x ∈ Y} sorryAll goals completed! 🐙

Compatibility of set difference

theorem declaration uses 'sorry'SetTheory.Set.coe_diff (X Y: Set) :
    (X \ Y : _root_.Set Object) = (X : _root_.Set Object) \ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} \ {x | x ∈ Y} = {x | x ∈ X} \ {x | x ∈ Y} sorryAll goals completed! 🐙

Compatibility of disjointness

theorem declaration uses 'sorry'SetTheory.Set.coe_Disjoint (X Y: Set) :
    Disjoint (X : _root_.Set Object) (Y : _root_.Set Object) ↔ Disjoint X Y := byinst✝:SetTheoryX:SetY:Set⊢ Disjoint {x | x ∈ X} {x | x ∈ Y} ↔ Disjoint X Y sorryAll goals completed! 🐙

end Chapter3