import data.set.lattice

import logic.small.basic

import order.well_founded

universes u v

def arity (α : Type u) : ℕ → Type u

| 0 := α

| (n+1) := α → arity n

@[simp] theorem arity_zero (α : Type u) : arity α 0 = α := rfl

@[simp] theorem arity_succ (α : Type u) (n : ℕ) : arity α n.succ = (α → arity α n) := rfl

namespace arity

def const {α : Type u} (a : α) : ∀ n, arity α n

| 0 := a

| (n+1) := λ _, const n

@[simp] theorem const_zero {α : Type u} (a : α) : const a 0 = a := rfl

@[simp] theorem const_succ {α : Type u} (a : α) (n : ℕ) : const a n.succ = λ _, const a n := rfl

theorem const_succ_apply {α : Type u} (a : α) (n : ℕ) (x : α) : const a n.succ x = const a n := rfl

instance arity.inhabited {α n} [inhabited α] : inhabited (arity α n) := ⟨const default _⟩

end arity

inductive pSet : Type (u+1)

| mk (α : Type u) (A : α → pSet) : pSet

namespace pSet

def type : pSet → Type u

| ⟨α, A⟩ := α

def func : Π (x : pSet), x.type → pSet

| ⟨α, A⟩ := A

@[simp] theorem mk_type (α A) : type ⟨α, A⟩ = α := rfl

@[simp] theorem mk_func (α A) : func ⟨α, A⟩ = A := rfl

@[simp] theorem eta : Π (x : pSet), mk x.type x.func = x

| ⟨α, A⟩ := rfl

def equiv (x y : pSet) : Prop :=

pSet.rec (λ α z m ⟨β, B⟩, (∀ a, ∃ b, m a (B b)) ∧ (∀ b, ∃ a, m a (B b))) x y

theorem equiv_iff : Π {x y : pSet}, equiv x y ↔

(∀ i, ∃ j, equiv (x.func i) (y.func j)) ∧ (∀ j, ∃ i, equiv (x.func i) (y.func j))

| ⟨α, A⟩ ⟨β, B⟩ := iff.rfl

theorem equiv.exists_left {x y : pSet} (h : equiv x y) : ∀ i, ∃ j, equiv (x.func i) (y.func j) :=

(equiv_iff.1 h).1

theorem equiv.exists_right {x y : pSet} (h : equiv x y) : ∀ j, ∃ i, equiv (x.func i) (y.func j) :=

(equiv_iff.1 h).2

@[refl] protected theorem equiv.refl (x) : equiv x x :=

pSet.rec_on x $ λ α A IH, ⟨λ a, ⟨a, IH a⟩, λ a, ⟨a, IH a⟩⟩

protected theorem equiv.rfl : ∀ {x}, equiv x x := equiv.refl

protected theorem equiv.euc {x} : Π {y z}, equiv x y → equiv z y → equiv x z :=

pSet.rec_on x $ λ α A IH y, pSet.cases_on y $ λ β B ⟨γ, Γ⟩ ⟨αβ, βα⟩ ⟨γβ, βγ⟩,

⟨λ a, let ⟨b, ab⟩ := αβ a, ⟨c, bc⟩ := βγ b in ⟨c, IH a ab bc⟩,

λ c, let ⟨b, cb⟩ := γβ c, ⟨a, ba⟩ := βα b in ⟨a, IH a ba cb⟩⟩

@[symm] protected theorem equiv.symm {x y} : equiv x y → equiv y x :=

(equiv.refl y).euc

protected theorem equiv.comm {x y} : equiv x y ↔ equiv y x :=

⟨equiv.symm, equiv.symm⟩

@[trans] protected theorem equiv.trans {x y z} (h1 : equiv x y) (h2 : equiv y z) : equiv x z :=

h1.euc h2.symm

protected theorem equiv_of_is_empty (x y : pSet) [is_empty x.type] [is_empty y.type] : equiv x y :=

equiv_iff.2 $ by simp

instance setoid : setoid pSet :=

⟨pSet.equiv, equiv.refl, λ x y, equiv.symm, λ x y z, equiv.trans⟩

protected def subset (x y : pSet) : Prop := ∀ a, ∃ b, equiv (x.func a) (y.func b)

instance : has_subset pSet := ⟨pSet.subset⟩

instance : is_refl pSet (⊆) := ⟨λ x a, ⟨a, equiv.refl _⟩⟩

instance : is_trans pSet (⊆) :=

⟨λ x y z hxy hyz a, begin

cases hxy a with b hb,

cases hyz b with c hc,

exact ⟨c, hb.trans hc⟩

end⟩

theorem equiv.ext : Π (x y : pSet), equiv x y ↔ (x ⊆ y ∧ y ⊆ x)

| ⟨α, A⟩ ⟨β, B⟩ :=

⟨λ ⟨αβ, βα⟩, ⟨αβ, λ b, let ⟨a, h⟩ := βα b in ⟨a, equiv.symm h⟩⟩,

λ ⟨αβ, βα⟩, ⟨αβ, λ b, let ⟨a, h⟩ := βα b in ⟨a, equiv.symm h⟩⟩⟩

theorem subset.congr_left : Π {x y z : pSet}, equiv x y → (x ⊆ z ↔ y ⊆ z)

| ⟨α, A⟩ ⟨β, B⟩ ⟨γ, Γ⟩ ⟨αβ, βα⟩ :=

⟨λ αγ b, let ⟨a, ba⟩ := βα b, ⟨c, ac⟩ := αγ a in ⟨c, (equiv.symm ba).trans ac⟩,

λ βγ a, let ⟨b, ab⟩ := αβ a, ⟨c, bc⟩ := βγ b in ⟨c, equiv.trans ab bc⟩⟩

theorem subset.congr_right : Π {x y z : pSet}, equiv x y → (z ⊆ x ↔ z ⊆ y)

| ⟨α, A⟩ ⟨β, B⟩ ⟨γ, Γ⟩ ⟨αβ, βα⟩ :=

⟨λ γα c, let ⟨a, ca⟩ := γα c, ⟨b, ab⟩ := αβ a in ⟨b, ca.trans ab⟩,

λ γβ c, let ⟨b, cb⟩ := γβ c, ⟨a, ab⟩ := βα b in ⟨a, cb.trans (equiv.symm ab)⟩⟩

protected def mem (x y : pSet.{u}) : Prop := ∃ b, equiv x (y.func b)

instance : has_mem pSet pSet := ⟨pSet.mem⟩

theorem mem.mk {α : Type u} (A : α → pSet) (a : α) : A a ∈ mk α A :=

⟨a, equiv.refl (A a)⟩

theorem func_mem (x : pSet) (i : x.type) : x.func i ∈ x :=

by { cases x, apply mem.mk }

theorem mem.ext : Π {x y : pSet.{u}}, (∀ w : pSet.{u}, w ∈ x ↔ w ∈ y) → equiv x y

| ⟨α, A⟩ ⟨β, B⟩ h := ⟨λ a, (h (A a)).1 (mem.mk A a),

λ b, let ⟨a, ha⟩ := (h (B b)).2 (mem.mk B b) in ⟨a, ha.symm⟩⟩

theorem mem.congr_right : Π {x y : pSet.{u}}, equiv x y → (∀ {w : pSet.{u}}, w ∈ x ↔ w ∈ y)

| ⟨α, A⟩ ⟨β, B⟩ ⟨αβ, βα⟩ w :=

⟨λ ⟨a, ha⟩, let ⟨b, hb⟩ := αβ a in ⟨b, ha.trans hb⟩,

λ ⟨b, hb⟩, let ⟨a, ha⟩ := βα b in ⟨a, hb.euc ha⟩⟩

theorem equiv_iff_mem {x y : pSet.{u}} : equiv x y ↔ (∀ {w : pSet.{u}}, w ∈ x ↔ w ∈ y) :=

⟨mem.congr_right, match x, y with

| ⟨α, A⟩, ⟨β, B⟩, h := ⟨λ a, h.1 (mem.mk A a), λ b,

let ⟨a, h⟩ := h.2 (mem.mk B b) in ⟨a, h.symm⟩⟩

end⟩

theorem mem.congr_left : Π {x y : pSet.{u}}, equiv x y → (∀ {w : pSet.{u}}, x ∈ w ↔ y ∈ w)

| x y h ⟨α, A⟩ := ⟨λ ⟨a, ha⟩, ⟨a, h.symm.trans ha⟩, λ ⟨a, ha⟩, ⟨a, h.trans ha⟩⟩

private theorem mem_wf_aux : Π {x y : pSet.{u}}, equiv x y → acc (∈) y

| ⟨α, A⟩ ⟨β, B⟩ H := ⟨_, begin

rintros ⟨γ, C⟩ ⟨b, hc⟩,

cases H.exists_right b with a ha,

have H := ha.trans hc.symm,

rw mk_func at H,

exact mem_wf_aux H

end⟩

theorem mem_wf : @well_founded pSet (∈) := ⟨λ x, mem_wf_aux $ equiv.refl x⟩

instance : has_well_founded pSet := ⟨_, mem_wf⟩

instance : is_asymm pSet (∈) := mem_wf.is_asymm

theorem mem_asymm {x y : pSet} : x ∈ y → y ∉ x := asymm

theorem mem_irrefl (x : pSet) : x ∉ x := irrefl x

def to_set (u : pSet.{u}) : set pSet.{u} := {x | x ∈ u}

@[simp] theorem mem_to_set (a u : pSet.{u}) : a ∈ u.to_set ↔ a ∈ u := iff.rfl

protected def nonempty (u : pSet) : Prop := u.to_set.nonempty

theorem nonempty_def (u : pSet) : u.nonempty ↔ ∃ x, x ∈ u := iff.rfl

theorem nonempty_of_mem {x u : pSet} (h : x ∈ u) : u.nonempty := ⟨x, h⟩

@[simp] theorem nonempty_to_set_iff {u : pSet} : u.to_set.nonempty ↔ u.nonempty := iff.rfl

theorem nonempty_type_iff_nonempty {x : pSet} : nonempty x.type ↔ pSet.nonempty x :=

⟨λ ⟨i⟩, ⟨_, func_mem _ i⟩, λ ⟨i, j, h⟩, ⟨j⟩⟩

theorem nonempty_of_nonempty_type (x : pSet) [h : nonempty x.type] : pSet.nonempty x :=

nonempty_type_iff_nonempty.1 h

theorem equiv.eq {x y : pSet} : equiv x y ↔ to_set x = to_set y :=

equiv_iff_mem.trans set.ext_iff.symm

instance : has_coe pSet (set pSet) := ⟨to_set⟩

protected def empty : pSet := ⟨_, pempty.elim⟩

instance : has_emptyc pSet := ⟨pSet.empty⟩

instance : inhabited pSet := ⟨∅⟩

instance : is_empty (type (∅)) := pempty.is_empty

@[simp] theorem not_mem_empty (x : pSet.{u}) : x ∉ (∅ : pSet.{u}) := is_empty.exists_iff.1

@[simp] theorem to_set_empty : to_set ∅ = ∅ := by simp [to_set]

@[simp] theorem empty_subset (x : pSet.{u}) : (∅ : pSet) ⊆ x := λ x, x.elim

@[simp] theorem not_nonempty_empty : ¬ pSet.nonempty ∅ := by simp [pSet.nonempty]

protected theorem equiv_empty (x : pSet) [is_empty x.type] : equiv x ∅ :=

pSet.equiv_of_is_empty x _

protected def insert (x y : pSet) : pSet := ⟨option y.type, λ o, option.rec x y.func o⟩

instance : has_insert pSet pSet := ⟨pSet.insert⟩

instance : has_singleton pSet pSet := ⟨λ s, insert s ∅⟩

instance : is_lawful_singleton pSet pSet := ⟨λ _, rfl⟩

instance (x y : pSet) : inhabited (insert x y).type := option.inhabited _

def of_nat : ℕ → pSet

| 0 := ∅

| (n+1) := insert (of_nat n) (of_nat n)

def omega : pSet := ⟨ulift ℕ, λ n, of_nat n.down⟩

protected def sep (p : pSet → Prop) (x : pSet) : pSet := ⟨{a // p (x.func a)}, λ y, x.func y.1⟩

instance : has_sep pSet pSet := ⟨pSet.sep⟩

def powerset (x : pSet) : pSet := ⟨set x.type, λ p, ⟨{a // p a}, λ y, x.func y.1⟩⟩

@[simp] theorem mem_powerset : Π {x y : pSet}, y ∈ powerset x ↔ y ⊆ x

| ⟨α, A⟩ ⟨β, B⟩ := ⟨λ ⟨p, e⟩, (subset.congr_left e).2 $ λ ⟨a, pa⟩, ⟨a, equiv.refl (A a)⟩,

λ βα, ⟨{a | ∃ b, equiv (B b) (A a)}, λ b, let ⟨a, ba⟩ := βα b in ⟨⟨a, b, ba⟩, ba⟩,

λ ⟨a, b, ba⟩, ⟨b, ba⟩⟩⟩

def sUnion (a : pSet) : pSet := ⟨Σ x, (a.func x).type, λ ⟨x, y⟩, (a.func x).func y⟩

prefix (name := pSet.sUnion) `⋃₀ `:110 := pSet.sUnion

@[simp] theorem mem_sUnion : Π {x y : pSet.{u}}, y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

| ⟨α, A⟩ y :=

⟨λ ⟨⟨a, c⟩, (e : equiv y ((A a).func c))⟩,

have func (A a) c ∈ mk (A a).type (A a).func, from mem.mk (A a).func c,

⟨_, mem.mk _ _, (mem.congr_left e).2 (by rwa eta at this)⟩,

λ ⟨⟨β, B⟩, ⟨a, (e : equiv (mk β B) (A a))⟩, ⟨b, yb⟩⟩,

by { rw ←(eta (A a)) at e, exact

let ⟨βt, tβ⟩ := e, ⟨c, bc⟩ := βt b in ⟨⟨a, c⟩, yb.trans bc⟩ }⟩

@[simp] theorem to_set_sUnion (x : pSet.{u}) : (⋃₀ x).to_set = ⋃₀ (to_set '' x.to_set) :=

by { ext, simp }

def image (f : pSet.{u} → pSet.{u}) (x : pSet.{u}) : pSet := ⟨x.type, f ∘ x.func⟩

theorem mem_image {f : pSet.{u} → pSet.{u}} (H : ∀ {x y}, equiv x y → equiv (f x) (f y)) :

Π {x y : pSet.{u}}, y ∈ image f x ↔ ∃ z ∈ x, equiv y (f z)

| ⟨α, A⟩ y := ⟨λ ⟨a, ya⟩, ⟨A a, mem.mk A a, ya⟩, λ ⟨z, ⟨a, za⟩, yz⟩, ⟨a, yz.trans (H za)⟩⟩

protected def lift : pSet.{u} → pSet.{max u v}

| ⟨α, A⟩ := ⟨ulift α, λ ⟨x⟩, lift (A x)⟩

@[nolint check_univs] -- intended to be used with explicit universe parameters

def embed : pSet.{max (u+1) v} := ⟨ulift.{v u+1} pSet, λ ⟨x⟩, pSet.lift.{u (max (u+1) v)} x⟩

theorem lift_mem_embed : Π (x : pSet.{u}), pSet.lift.{u (max (u+1) v)} x ∈ embed.{u v} :=

λ x, ⟨⟨x⟩, equiv.rfl⟩

def arity.equiv : Π {n}, arity pSet.{u} n → arity pSet.{u} n → Prop

| 0 a b := equiv a b

| (n+1) a b := ∀ x y, equiv x y → arity.equiv (a x) (b y)

lemma arity.equiv_const {a : pSet.{u}} : ∀ n, arity.equiv (arity.const a n) (arity.const a n)

| 0 := equiv.rfl

| (n+1) := λ x y h, arity.equiv_const _

def resp (n) := {x : arity pSet.{u} n // arity.equiv x x}

instance resp.inhabited {n} : inhabited (resp n) :=

⟨⟨arity.const default _, arity.equiv_const _⟩⟩

def resp.f {n} (f : resp (n+1)) (x : pSet) : resp n :=

⟨f.1 x, f.2 _ _ $ equiv.refl x⟩

def resp.equiv {n} (a b : resp n) : Prop := arity.equiv a.1 b.1

protected theorem resp.equiv.refl {n} (a : resp n) : resp.equiv a a := a.2

protected theorem resp.equiv.euc : Π {n} {a b c : resp n},

resp.equiv a b → resp.equiv c b → resp.equiv a c

| 0 a b c hab hcb := equiv.euc hab hcb

| (n+1) a b c hab hcb := λ x y h,

@resp.equiv.euc n (a.f x) (b.f y) (c.f y) (hab _ _ h) (hcb _ _ $ equiv.refl y)

protected theorem resp.equiv.symm {n} {a b : resp n} : resp.equiv a b → resp.equiv b a :=

(resp.equiv.refl b).euc

protected theorem resp.equiv.trans {n} {x y z : resp n}

(h1 : resp.equiv x y) (h2 : resp.equiv y z) : resp.equiv x z :=

h1.euc h2.symm

instance resp.setoid {n} : setoid (resp n) :=

⟨resp.equiv, resp.equiv.refl, λ x y, resp.equiv.symm, λ x y z, resp.equiv.trans⟩

end pSet

def Set : Type (u+1) := quotient pSet.setoid.{u}

namespace pSet

namespace resp

def eval_aux : Π {n}, {f : resp n → arity Set.{u} n // ∀ (a b : resp n), resp.equiv a b → f a = f b}

| 0 := ⟨λ a, ⟦a.1⟧, λ a b h, quotient.sound h⟩

| (n+1) := let F : resp (n + 1) → arity Set (n + 1) := λ a, @quotient.lift _ _ pSet.setoid

(λ x, eval_aux.1 (a.f x)) (λ b c h, eval_aux.2 _ _ (a.2 _ _ h)) in

⟨F, λ b c h, funext $ @quotient.ind _ _ (λ q, F b q = F c q) $ λ z,

eval_aux.2 (resp.f b z) (resp.f c z) (h _ _ (pSet.equiv.refl z))⟩

def eval (n) : resp n → arity Set.{u} n := eval_aux.1

theorem eval_val {n f x} : (@eval (n+1) f : Set → arity Set n) ⟦x⟧ = eval n (resp.f f x) := rfl

end resp

class inductive definable (n) : arity Set.{u} n → Type (u+1)

| mk (f) : definable (resp.eval n f)

attribute [instance] definable.mk

def definable.eq_mk {n} (f) : Π {s : arity Set.{u} n} (H : resp.eval _ f = s), definable n s

| ._ rfl := ⟨f⟩

def definable.resp {n} : Π (s : arity Set.{u} n) [definable n s], resp n

| ._ ⟨f⟩ := f

theorem definable.eq {n} :

Π (s : arity Set.{u} n) [H : definable n s], (@definable.resp n s H).eval _ = s

| ._ ⟨f⟩ := rfl

end pSet

namespace classical

open pSet

noncomputable def all_definable : Π {n} (F : arity Set.{u} n), definable n F

| 0 F := let p := @quotient.exists_rep pSet _ F in

definable.eq_mk ⟨some p, equiv.rfl⟩ (some_spec p)

| (n+1) (F : arity Set.{u} (n + 1)) := begin

have I := λ x, (all_definable (F x)),

refine definable.eq_mk ⟨λ x : pSet, (@definable.resp _ _ (I ⟦x⟧)).1, _⟩ _,

{ dsimp [arity.equiv],

introsI x y h,

rw @quotient.sound pSet _ _ _ h,

exact (definable.resp (F ⟦y⟧)).2 },

refine funext (λ q, quotient.induction_on q $ λ x, _),

simp_rw [resp.eval_val, resp.f, subtype.val_eq_coe, subtype.coe_eta],

exact @definable.eq _ (F ⟦x⟧) (I ⟦x⟧),

end

end classical

namespace Set

open pSet

def mk : pSet → Set := quotient.mk

@[simp] theorem mk_eq (x : pSet) : @eq Set ⟦x⟧ (mk x) := rfl

@[simp] theorem mk_out : ∀ x : Set, mk x.out = x := quotient.out_eq

theorem eq {x y : pSet} : mk x = mk y ↔ equiv x y := quotient.eq

theorem sound {x y : pSet} (h : pSet.equiv x y) : mk x = mk y := quotient.sound h

theorem exact {x y : pSet} : mk x = mk y → pSet.equiv x y := quotient.exact

@[simp] lemma eval_mk {n f x} :

(@resp.eval (n+1) f : Set → arity Set n) (mk x) = resp.eval n (resp.f f x) :=

rfl

protected def mem : Set → Set → Prop :=

quotient.lift₂ pSet.mem

(λ x y x' y' hx hy, propext ((mem.congr_left hx).trans (mem.congr_right hy)))

instance : has_mem Set Set := ⟨Set.mem⟩

@[simp] theorem mk_mem_iff {x y : pSet} : mk x ∈ mk y ↔ x ∈ y := iff.rfl

def to_set (u : Set.{u}) : set Set.{u} := {x | x ∈ u}

@[simp] theorem mem_to_set (a u : Set.{u}) : a ∈ u.to_set ↔ a ∈ u := iff.rfl

instance small_to_set (x : Set.{u}) : small.{u} x.to_set :=

quotient.induction_on x $ λ a, begin

let f : a.type → (mk a).to_set := λ i, ⟨mk $ a.func i, func_mem a i⟩,

suffices : function.surjective f,

{ exact small_of_surjective this },

rintro ⟨y, hb⟩,

induction y using quotient.induction_on,

cases hb with i h,

exact ⟨i, subtype.coe_injective (quotient.sound h.symm)⟩

protected def nonempty (u : Set) : Prop := u.to_set.nonempty

theorem nonempty_def (u : Set) : u.nonempty ↔ ∃ x, x ∈ u := iff.rfl

theorem nonempty_of_mem {x u : Set} (h : x ∈ u) : u.nonempty := ⟨x, h⟩

@[simp] theorem nonempty_to_set_iff {u : Set} : u.to_set.nonempty ↔ u.nonempty := iff.rfl

protected def subset (x y : Set.{u}) :=

∀ ⦃z⦄, z ∈ x → z ∈ y

instance has_subset : has_subset Set :=

⟨Set.subset⟩

lemma subset_def {x y : Set.{u}} : x ⊆ y ↔ ∀ ⦃z⦄, z ∈ x → z ∈ y := iff.rfl

instance : is_refl Set (⊆) := ⟨λ x a, id⟩

instance : is_trans Set (⊆) := ⟨λ x y z hxy hyz a ha, hyz (hxy ha)⟩

@[simp] theorem subset_iff : Π {x y : pSet}, mk x ⊆ mk y ↔ x ⊆ y

| ⟨α, A⟩ ⟨β, B⟩ := ⟨λ h a, @h ⟦A a⟧ (mem.mk A a),

λ h z, quotient.induction_on z (λ z ⟨a, za⟩, let ⟨b, ab⟩ := h a in ⟨b, za.trans ab⟩)⟩

@[simp] theorem to_set_subset_iff {x y : Set} : x.to_set ⊆ y.to_set ↔ x ⊆ y :=

by simp [subset_def, set.subset_def]

@[ext] theorem ext {x y : Set.{u}} : (∀ z : Set.{u}, z ∈ x ↔ z ∈ y) → x = y :=

quotient.induction_on₂ x y (λ u v h, quotient.sound (mem.ext (λ w, h ⟦w⟧)))

theorem ext_iff {x y : Set.{u}} : x = y ↔ (∀ z : Set.{u}, z ∈ x ↔ z ∈ y) :=

⟨λ h, by simp [h], ext⟩

theorem to_set_injective : function.injective to_set := λ x y h, ext $ set.ext_iff.1 h

@[simp] theorem to_set_inj {x y : Set} : x.to_set = y.to_set ↔ x = y :=

to_set_injective.eq_iff

instance : is_antisymm Set (⊆) := ⟨λ a b hab hba, ext $ λ c, ⟨@hab c, @hba c⟩⟩

protected def empty : Set := mk ∅

instance : has_emptyc Set := ⟨Set.empty⟩

instance : inhabited Set := ⟨∅⟩

@[simp] theorem not_mem_empty (x) : x ∉ (∅ : Set.{u}) :=

quotient.induction_on x pSet.not_mem_empty

@[simp] theorem to_set_empty : to_set ∅ = ∅ := by simp [to_set]

@[simp] theorem empty_subset (x : Set.{u}) : (∅ : Set) ⊆ x :=

quotient.induction_on x $ λ y, subset_iff.2 $ pSet.empty_subset y

@[simp] theorem not_nonempty_empty : ¬ Set.nonempty ∅ := by simp [Set.nonempty]

@[simp] theorem nonempty_mk_iff {x : pSet} : (mk x).nonempty ↔ x.nonempty :=

refine ⟨_, λ ⟨a, h⟩, ⟨mk a, h⟩⟩,

rintro ⟨a, h⟩,

induction a using quotient.induction_on,

exact ⟨a, h⟩

theorem eq_empty (x : Set.{u}) : x = ∅ ↔ ∀ y : Set.{u}, y ∉ x := by { rw ext_iff, simp }

theorem eq_empty_or_nonempty (u : Set) : u = ∅ ∨ u.nonempty :=

by { rw [eq_empty, ←not_exists], apply em' }

protected def insert : Set → Set → Set :=

resp.eval 2 ⟨pSet.insert, λ u v uv ⟨α, A⟩ ⟨β, B⟩ ⟨αβ, βα⟩,

⟨λ o, match o with

| some a := let ⟨b, hb⟩ := αβ a in ⟨some b, hb⟩

| none := ⟨none, uv⟩

end, λ o, match o with

| some b := let ⟨a, ha⟩ := βα b in ⟨some a, ha⟩

| none := ⟨none, uv⟩

end⟩⟩

instance : has_insert Set Set := ⟨Set.insert⟩

instance : has_singleton Set Set := ⟨λ x, insert x ∅⟩

instance : is_lawful_singleton Set Set := ⟨λ x, rfl⟩

@[simp] theorem mem_insert_iff {x y z : Set.{u}} : x ∈ insert y z ↔ x = y ∨ x ∈ z :=

quotient.induction_on₃ x y z

(λ x y ⟨α, A⟩, show x ∈ pSet.mk (option α) (λ o, option.rec y A o) ↔

mk x = mk y ∨ x ∈ pSet.mk α A, from

⟨λ m, match m with

| ⟨some a, ha⟩ := or.inr ⟨a, ha⟩

| ⟨none, h⟩ := or.inl (quotient.sound h)

end, λ m, match m with

| or.inr ⟨a, ha⟩ := ⟨some a, ha⟩

| or.inl h := ⟨none, quotient.exact h⟩

end⟩)

theorem mem_insert (x y : Set) : x ∈ insert x y := mem_insert_iff.2 $ or.inl rfl

theorem mem_insert_of_mem {y z : Set} (x) (h : z ∈ y): z ∈ insert x y := mem_insert_iff.2 $ or.inr h

@[simp] theorem to_set_insert (x y : Set) : (insert x y).to_set = insert x y.to_set :=

by { ext, simp }

@[simp] theorem mem_singleton {x y : Set.{u}} : x ∈ @singleton Set.{u} Set.{u} _ y ↔ x = y :=

iff.trans mem_insert_iff ⟨λ o, or.rec (λ h, h) (λ n, absurd n (not_mem_empty _)) o, or.inl⟩

@[simp] theorem to_set_singleton (x : Set) : ({x} : Set).to_set = {x} :=

by { ext, simp }

theorem insert_nonempty (u v : Set) : (insert u v).nonempty := ⟨u, mem_insert u v⟩

theorem singleton_nonempty (u : Set) : Set.nonempty {u} := insert_nonempty u ∅

@[simp] theorem mem_pair {x y z : Set.{u}} : x ∈ ({y, z} : Set) ↔ x = y ∨ x = z :=

iff.trans mem_insert_iff $ or_congr iff.rfl mem_singleton

def omega : Set := mk omega

@[simp] theorem omega_zero : ∅ ∈ omega :=

⟨⟨0⟩, equiv.rfl⟩

@[simp] theorem omega_succ {n} : n ∈ omega.{u} → insert n n ∈ omega.{u} :=

quotient.induction_on n (λ x ⟨⟨n⟩, h⟩, ⟨⟨n+1⟩, Set.exact $

show insert (mk x) (mk x) = insert (mk $ of_nat n) (mk $ of_nat n), { rw Set.sound h, refl } ⟩)

protected def sep (p : Set → Prop) : Set → Set :=

resp.eval 1 ⟨pSet.sep (λ y, p (mk y)), λ ⟨α, A⟩ ⟨β, B⟩ ⟨αβ, βα⟩,

⟨λ ⟨a, pa⟩, let ⟨b, hb⟩ := αβ a in ⟨⟨b, by rwa [mk_func, ←Set.sound hb]⟩, hb⟩,

λ ⟨b, pb⟩, let ⟨a, ha⟩ := βα b in ⟨⟨a, by rwa [mk_func, Set.sound ha]⟩, ha⟩⟩⟩

instance : has_sep Set Set := ⟨Set.sep⟩

@[simp] theorem mem_sep {p : Set.{u} → Prop} {x y : Set.{u}} : y ∈ {y ∈ x | p y} ↔ y ∈ x ∧ p y :=

quotient.induction_on₂ x y (λ ⟨α, A⟩ y,

⟨λ ⟨⟨a, pa⟩, h⟩, ⟨⟨a, h⟩, by rwa (@quotient.sound pSet _ _ _ h)⟩,

λ ⟨⟨a, h⟩, pa⟩, ⟨⟨a, by { rw mk_func at h, rwa [mk_func, ←Set.sound h] }⟩, h⟩⟩)

@[simp] theorem to_set_sep (a : Set) (p : Set → Prop) :

{x ∈ a | p x}.to_set = {x ∈ a.to_set | p x} :=

by { ext, simp }

def powerset : Set → Set :=

resp.eval 1 ⟨powerset, λ ⟨α, A⟩ ⟨β, B⟩ ⟨αβ, βα⟩,

⟨λ p, ⟨{b | ∃ a, p a ∧ equiv (A a) (B b)},

λ ⟨a, pa⟩, let ⟨b, ab⟩ := αβ a in ⟨⟨b, a, pa, ab⟩, ab⟩,

λ ⟨b, a, pa, ab⟩, ⟨⟨a, pa⟩, ab⟩⟩,

λ q, ⟨{a | ∃ b, q b ∧ equiv (A a) (B b)},

λ ⟨a, b, qb, ab⟩, ⟨⟨b, qb⟩, ab⟩,

λ ⟨b, qb⟩, let ⟨a, ab⟩ := βα b in ⟨⟨a, b, qb, ab⟩, ab⟩⟩⟩⟩

@[simp] theorem mem_powerset {x y : Set.{u}} : y ∈ powerset x ↔ y ⊆ x :=

quotient.induction_on₂ x y ( λ ⟨α, A⟩ ⟨β, B⟩,

show (⟨β, B⟩ : pSet.{u}) ∈ (pSet.powerset.{u} ⟨α, A⟩) ↔ _,

by simp [mem_powerset, subset_iff])

theorem sUnion_lem {α β : Type u} (A : α → pSet) (B : β → pSet) (αβ : ∀ a, ∃ b, equiv (A a) (B b)) :

∀ a, ∃ b, (equiv ((sUnion ⟨α, A⟩).func a) ((sUnion ⟨β, B⟩).func b))

| ⟨a, c⟩ := let ⟨b, hb⟩ := αβ a in

begin

induction ea : A a with γ Γ,

induction eb : B b with δ Δ,

rw [ea, eb] at hb,

cases hb with γδ δγ,

exact

let c : type (A a) := c, ⟨d, hd⟩ := γδ (by rwa ea at c) in

have pSet.equiv ((A a).func c) ((B b).func (eq.rec d (eq.symm eb))), from

match A a, B b, ea, eb, c, d, hd with ._, ._, rfl, rfl, x, y, hd := hd end,

⟨⟨b, by { rw mk_func, exact eq.rec d (eq.symm eb) }⟩, this⟩

end

def sUnion : Set → Set :=

resp.eval 1 ⟨pSet.sUnion, λ ⟨α, A⟩ ⟨β, B⟩ ⟨αβ, βα⟩,

⟨sUnion_lem A B αβ, λ a, exists.elim (sUnion_lem B A (λ b,

exists.elim (βα b) (λ c hc, ⟨c, pSet.equiv.symm hc⟩)) a) (λ b hb, ⟨b, pSet.equiv.symm hb⟩)⟩⟩

prefix (name := Set.sUnion) `⋃₀ `:110 := Set.sUnion

noncomputable def sInter (x : Set) : Set :=

by { classical, exact dite x.nonempty (λ h, {y ∈ h.some | ∀ z ∈ x, y ∈ z}) (λ _, ∅) }

prefix (name := Set.sInter) `⋂₀ `:110 := Set.sInter

@[simp] theorem mem_sUnion {x y : Set.{u}} : y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z :=

quotient.induction_on₂ x y (λ x y, iff.trans mem_sUnion

⟨λ ⟨z, h⟩, ⟨⟦z⟧, h⟩, λ ⟨z, h⟩, quotient.induction_on z (λ z h, ⟨z, h⟩) h⟩)

theorem mem_sInter {x y : Set} (h : x.nonempty) : y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z :=

rw [sInter, dif_pos h],

simp only [mem_to_set, mem_sep, and_iff_right_iff_imp],

exact λ H, H _ h.some_mem

@[simp] theorem sUnion_empty : ⋃₀ (∅ : Set) = ∅ := by { ext, simp }

@[simp] theorem sInter_empty : ⋂₀ (∅ : Set) = ∅ := dif_neg $ by simp

theorem mem_of_mem_sInter {x y z : Set} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) : y ∈ z :=

rcases eq_empty_or_nonempty x with rfl | hx,

{ exact (not_mem_empty z hz).elim },

{ exact (mem_sInter hx).1 hy z hz }

theorem mem_sUnion_of_mem {x y z : Set} (hy : y ∈ z) (hz : z ∈ x) : y ∈ ⋃₀ x :=

mem_sUnion.2 ⟨z, hz, hy⟩

theorem not_mem_sInter_of_not_mem {x y z : Set} (hy : ¬ y ∈ z) (hz : z ∈ x) : ¬ y ∈ ⋂₀ x :=

λ hx, hy $ mem_of_mem_sInter hx hz

@[simp] theorem sUnion_singleton {x : Set.{u}} : ⋃₀ ({x} : Set) = x :=

ext $ λ y, by simp_rw [mem_sUnion, exists_prop, mem_singleton, exists_eq_left]

@[simp] theorem sInter_singleton {x : Set.{u}} : ⋂₀ ({x} : Set) = x :=

ext $ λ y, by simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]

@[simp] theorem to_set_sUnion (x : Set.{u}) : (⋃₀ x).to_set = ⋃₀ (to_set '' x.to_set) :=

by { ext, simp }

theorem to_set_sInter {x : Set.{u}} (h : x.nonempty) : (⋂₀ x).to_set = ⋂₀ (to_set '' x.to_set) :=

by { ext, simp [mem_sInter h] }

theorem singleton_injective : function.injective (@singleton Set Set _) :=

λ x y H, let this := congr_arg sUnion H in by rwa [sUnion_singleton, sUnion_singleton] at this

@[simp] theorem singleton_inj {x y : Set} : ({x} : Set) = {y} ↔ x = y := singleton_injective.eq_iff

protected def union (x y : Set.{u}) : Set.{u} := ⋃₀ {x, y}

protected def inter (x y : Set.{u}) : Set.{u} := {z ∈ x | z ∈ y}

protected def diff (x y : Set.{u}) : Set.{u} := {z ∈ x | z ∉ y}

instance : has_union Set := ⟨Set.union⟩

instance : has_inter Set := ⟨Set.inter⟩

instance : has_sdiff Set := ⟨Set.diff⟩

@[simp] theorem to_set_union (x y : Set.{u}) : (x ∪ y).to_set = x.to_set ∪ y.to_set :=

by { unfold has_union.union, rw Set.union, simp }

@[simp] theorem to_set_inter (x y : Set.{u}) : (x ∩ y).to_set = x.to_set ∩ y.to_set :=

by { unfold has_inter.inter, rw Set.inter, ext, simp }

@[simp] theorem to_set_sdiff (x y : Set.{u}) : (x \ y).to_set = x.to_set \ y.to_set :=

by { change {z ∈ x | z ∉ y}.to_set = _, ext, simp }

@[simp] theorem mem_union {x y z : Set.{u}} : z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y :=

by { rw ←mem_to_set, simp }

@[simp] theorem mem_inter {x y z : Set.{u}} : z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y :=

@@mem_sep (λ z : Set.{u}, z ∈ y)

@[simp] theorem mem_diff {x y z : Set.{u}} : z ∈ x \ y ↔ z ∈ x ∧ z ∉ y :=

@@mem_sep (λ z : Set.{u}, z ∉ y)

@[simp] theorem sUnion_pair {x y : Set.{u}} : ⋃₀ ({x, y} : Set.{u}) = x ∪ y :=

ext,

simp_rw [mem_union, mem_sUnion, mem_pair],

split,

{ rintro ⟨w, (rfl | rfl), hw⟩,

{ exact or.inl hw },

{ exact or.inr hw } },

{ rintro (hz | hz),

{ exact ⟨x, or.inl rfl, hz⟩ },

{ exact ⟨y, or.inr rfl, hz⟩ } }

theorem mem_wf : @well_founded Set (∈) :=

well_founded_lift₂_iff.mpr pSet.mem_wf

theorem induction_on {p : Set → Prop} (x) (h : ∀ x, (∀ y ∈ x, p y) → p x) : p x :=

mem_wf.induction x h

instance : has_well_founded Set := ⟨_, mem_wf⟩

instance : is_asymm Set (∈) := mem_wf.is_asymm

theorem mem_asymm {x y : Set} : x ∈ y → y ∉ x := asymm

theorem mem_irrefl (x : Set) : x ∉ x := irrefl x

theorem regularity (x : Set.{u}) (h : x ≠ ∅) : ∃ y ∈ x, x ∩ y = ∅ :=

classical.by_contradiction $ λ ne, h $ (eq_empty x).2 $ λ y,

induction_on y $ λ z (IH : ∀ w : Set.{u}, w ∈ z → w ∉ x), show z ∉ x, from λ zx,

ne ⟨z, zx, (eq_empty _).2 (λ w wxz, let ⟨wx, wz⟩ := mem_inter.1 wxz in IH w wz wx)⟩

def image (f : Set → Set) [H : definable 1 f] : Set → Set :=

let r := @definable.resp 1 f _ in

resp.eval 1 ⟨image r.1, λ x y e, mem.ext $ λ z,

iff.trans (mem_image r.2) $ iff.trans (by exact

⟨λ ⟨w, h1, h2⟩, ⟨w, (mem.congr_right e).1 h1, h2⟩,

λ ⟨w, h1, h2⟩, ⟨w, (mem.congr_right e).2 h1, h2⟩⟩) $

iff.symm (mem_image r.2)⟩

theorem image.mk :

Π (f : Set.{u} → Set.{u}) [H : definable 1 f] (x) {y} (h : y ∈ x), f y ∈ @image f H x

| ._ ⟨F⟩ x y := quotient.induction_on₂ x y $ λ ⟨α, A⟩ y ⟨a, ya⟩, ⟨a, F.2 _ _ ya⟩

@[simp] theorem mem_image : Π {f : Set.{u} → Set.{u}} [H : definable 1 f] {x y : Set.{u}},

y ∈ @image f H x ↔ ∃ z ∈ x, f z = y

| ._ ⟨F⟩ x y := quotient.induction_on₂ x y $ λ ⟨α, A⟩ y,

⟨λ ⟨a, ya⟩, ⟨⟦A a⟧, mem.mk A a, eq.symm $ quotient.sound ya⟩,

λ ⟨z, hz, e⟩, e ▸ image.mk _ _ hz⟩

@[simp] theorem to_set_image (f : Set → Set) [H : definable 1 f] (x : Set) :

(image f x).to_set = f '' x.to_set :=

by { ext, simp }

noncomputable def range {α : Type u} (f : α → Set.{max u v}) : Set.{max u v} :=

⟦⟨ulift α, quotient.out ∘ f ∘ ulift.down⟩⟧

@[simp] theorem mem_range {α : Type u} {f : α → Set.{max u v}} {x : Set.{max u v}} :

x ∈ range f ↔ x ∈ set.range f :=

quotient.induction_on x (λ y, begin

split,

{ rintro ⟨z, hz⟩,

exact ⟨z.down, quotient.eq_mk_iff_out.2 hz.symm⟩ },

{ rintro ⟨z, hz⟩,

use z,

simpa [hz] using pSet.equiv.symm (quotient.mk_out y) }

end)

@[simp] theorem to_set_range {α : Type u} (f : α → Set.{max u v}) :

(range f).to_set = set.range f :=

by { ext, simp }

def pair (x y : Set.{u}) : Set.{u} := {{x}, {x, y}}

@[simp] theorem to_set_pair (x y : Set.{u}) : (pair x y).to_set = {{x}, {x, y}} := by simp [pair]

def pair_sep (p : Set.{u} → Set.{u} → Prop) (x y : Set.{u}) : Set.{u} :=

{z ∈ powerset (powerset (x ∪ y)) | ∃ a ∈ x, ∃ b ∈ y, z = pair a b ∧ p a b}

@[simp] theorem mem_pair_sep {p} {x y z : Set.{u}} :

z ∈ pair_sep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = pair a b ∧ p a b :=

refine mem_sep.trans ⟨and.right, λ e, ⟨_, e⟩⟩,

rcases e with ⟨a, ax, b, bY, rfl, pab⟩,

simp only [mem_powerset, subset_def, mem_union, pair, mem_pair],

rintros u (rfl|rfl) v; simp only [mem_singleton, mem_pair],

{ rintro rfl, exact or.inl ax },

{ rintro (rfl|rfl); [left, right]; assumption }

theorem pair_injective : function.injective2 pair :=

λ x x' y y' H, begin

have ae := ext_iff.1 H,

simp only [pair, mem_pair] at ae,

obtain rfl : x = x',

{ cases (ae {x}).1 (by simp) with h h,

{ exact singleton_injective h },

{ have m : x' ∈ ({x} : Set),

{ simp [h] },

rw mem_singleton.mp m } },

have he : x = y → y = y',

{ rintro rfl,

cases (ae {x, y'}).2 (by simp only [eq_self_iff_true, or_true]) with xy'x xy'xx,

{ rw [eq_comm, ←mem_singleton, ←xy'x, mem_pair],

exact or.inr rfl },

{ simpa [eq_comm] using (ext_iff.1 xy'xx y').1 (by simp) } },

obtain xyx | xyy' := (ae {x, y}).1 (by simp),

{ obtain rfl := mem_singleton.mp ((ext_iff.1 xyx y).1 $ by simp),

simp [he rfl] },

{ obtain rfl | yy' := mem_pair.mp ((ext_iff.1 xyy' y).1 $ by simp),

{ simp [he rfl] },

{ simp [yy'] } }

@[simp] theorem pair_inj {x y x' y' : Set} : pair x y = pair x' y' ↔ x = x' ∧ y = y' :=

pair_injective.eq_iff

def prod : Set.{u} → Set.{u} → Set.{u} := pair_sep (λ a b, true)

@[simp] theorem mem_prod {x y z : Set.{u}} : z ∈ prod x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = pair a b :=

by simp [prod]

@[simp] theorem pair_mem_prod {x y a b : Set.{u}} : pair a b ∈ prod x y ↔ a ∈ x ∧ b ∈ y :=

⟨λ h, let ⟨a', a'x, b', b'y, e⟩ := mem_prod.1 h in

match a', b', pair_injective e, a'x, b'y with ._, ._, ⟨rfl, rfl⟩, ax, bY := ⟨ax, bY⟩ end,

λ ⟨ax, bY⟩, mem_prod.2 ⟨a, ax, b, bY, rfl⟩⟩

def is_func (x y f : Set.{u}) : Prop :=

f ⊆ prod x y ∧ ∀ z : Set.{u}, z ∈ x → ∃! w, pair z w ∈ f

def funs (x y : Set.{u}) : Set.{u} :=

{f ∈ powerset (prod x y) | is_func x y f}

@[simp] theorem mem_funs {x y f : Set.{u}} : f ∈ funs x y ↔ is_func x y f :=

by simp [funs, is_func]

noncomputable instance map_definable_aux (f : Set → Set) [H : definable 1 f] :

definable 1 (λ y, pair y (f y)) :=

@classical.all_definable 1 _

noncomputable def map (f : Set → Set) [H : definable 1 f] : Set → Set :=

image (λ y, pair y (f y))

@[simp] theorem mem_map {f : Set → Set} [H : definable 1 f] {x y : Set} :

y ∈ map f x ↔ ∃ z ∈ x, pair z (f z) = y :=

mem_image

theorem map_unique {f : Set.{u} → Set.{u}} [H : definable 1 f] {x z : Set.{u}} (zx : z ∈ x) :

∃! w, pair z w ∈ map f x :=

⟨f z, image.mk _ _ zx, λ y yx, let ⟨w, wx, we⟩ := mem_image.1 yx, ⟨wz, fy⟩ := pair_injective we in

by rw[←fy, wz]⟩

@[simp] theorem map_is_func {f : Set → Set} [H : definable 1 f] {x y : Set} :

is_func x y (map f x) ↔ ∀ z ∈ x, f z ∈ y :=

⟨λ ⟨ss, h⟩ z zx, let ⟨t, t1, t2⟩ := h z zx in

(t2 (f z) (image.mk _ _ zx)).symm ▸ (pair_mem_prod.1 (ss t1)).right,

λ h, ⟨λ y yx, let ⟨z, zx, ze⟩ := mem_image.1 yx in ze ▸ pair_mem_prod.2 ⟨zx, h z zx⟩,

λ z, map_unique⟩⟩

def hereditarily (p : Set → Prop) : Set → Prop

| x := p x ∧ ∀ y ∈ x, hereditarily y

using_well_founded { dec_tac := `[assumption] }

section hereditarily

variables {p : Set.{u} → Prop} {x y : Set.{u}}

lemma hereditarily_iff :

hereditarily p x ↔ p x ∧ ∀ y ∈ x, hereditarily p y :=

by rw [← hereditarily]

alias hereditarily_iff ↔ hereditarily.def _

lemma hereditarily.self (h : x.hereditarily p) : p x := h.def.1

lemma hereditarily.mem (h : x.hereditarily p) (hy : y ∈ x) : y.hereditarily p := h.def.2 _ hy

lemma hereditarily.empty : hereditarily p x → p ∅ :=

apply x.induction_on,

intros y IH h,

rcases Set.eq_empty_or_nonempty y with (rfl|⟨a, ha⟩),

{ exact h.self },

{ exact IH a ha (h.mem ha) }

end hereditarily

end Set

has_compl, has_sdiff]]

def Class := set Set

namespace Class

@[ext] theorem ext {x y : Class.{u}} : (∀ z : Set.{u}, x z ↔ y z) → x = y := set.ext

theorem ext_iff {x y : Class.{u}} : x = y ↔ ∀ z, x z ↔ y z := set.ext_iff

def of_Set (x : Set.{u}) : Class.{u} := {y | y ∈ x}

instance : has_coe Set Class := ⟨of_Set⟩

def univ : Class := set.univ

def to_Set (B : Class.{u}) (A : Class.{u}) : Prop := ∃ x, ↑x = A ∧ B x

protected def mem (A B : Class.{u}) : Prop := to_Set.{u} B A

instance : has_mem Class Class := ⟨Class.mem⟩

theorem mem_def (A B : Class.{u}) : A ∈ B ↔ ∃ x, ↑x = A ∧ B x := iff.rfl

@[simp] theorem not_mem_empty (x : Class.{u}) : x ∉ (∅ : Class.{u}) := λ ⟨_, _, h⟩, h

@[simp] theorem not_empty_hom (x : Set.{u}) : ¬ (∅ : Class.{u}) x := id

@[simp] theorem mem_univ {A : Class.{u}} : A ∈ univ.{u} ↔ ∃ x : Set.{u}, ↑x = A :=

exists_congr $ λ x, and_true _

@[simp] theorem mem_univ_hom (x : Set.{u}) : univ.{u} x := trivial

theorem eq_univ_iff_forall {A : Class.{u}} : A = univ ↔ ∀ x : Set, A x := set.eq_univ_iff_forall