How to get an element from an existential proposition in Type theory proof assistant (Lean prover)

I am trying to implement set theory in type theory from scratch, just for self pedagogical purposes. Specifically, I'm using the Lean Prover, and defining the element-of relation from scratch using the symbol $\epsilon$, just for pedagogical purposes.

What I'm trying to do

However, I'm unsure how to even define the notion of inductive set in this way. I am using the definition of inductive set:


a set $S$ is inductive if $\emptyset \in S \land \forall x\in S, x\cup \{x\} \in S$.
The axiom of infinity then states that there exists an inductive set.

Where I'm getting stuck is at even defining the set $\{x\}$ in Lean. I know from the axiom of pairing, that there exists a set, which we denote by $\{x\}$, which is shorthand for $\{x,x\}$, such that $\forall u, (u\in \{x,x\} \iff u = x \lor u = x)$.

What goes wrong

However, in type theory this axiom doesn't give me the actual set, it gives me an inhabitant of the existential proposition type. I've tried to use the "let" command to extract from this the actual set, but I get the error: "invalid match/convoy expression, expected type is not known".
This makes me suspect I shouldn't be using this command here at all (I think it's only intended for proofs).

Maybe instead I should be using the axiom of choice?

My code

constant Set : Type
constant In : Set → Set → Prop
infix  `ε`:50  := In 

axiom pairing : ∀X:Set, ∀Y:Set, ∃S:Set, ∀u, u ε S ↔ u = X ∨ u = Y
axiom union : ∀X, ∀Y, ∃S, ∀u, u ε S ↔ u ε X ∨ u ε Y
infix `U`:49 := union

definition inductiveset (S:Set) : Prop := ∀x:Set, 
let ⟨ (Q:Set), (h: ∀u, u ε S ↔ (u = x ∨ u = x) ) ⟩ := (pairing x x) in
     x ε S → (x U Q) ε S 

axiom infinity : ∃S, inductiveset S

Summary

So basically:

-
How do I actually define the inductive set property in Lean?

-
Can I just extract a function $f:X\to Y$ from proof of a proposition $\forall x:X,\exists y:Y, ...$?

-
should I use the axiom of choice here?

Edit: Defining an operation from an existence theorem.

uniqu

The existential form of the axioms of set theory is convenient for the meta-theoretic explorations of set theory, such as forcing etc., where it is important to have a minimal language to worry about (only $\in$ relation). But even just stating the axioms of set theory without any constants and operation symbols is pretty haunting, see this gist of mine.

If you want a workable set theory you will have to rephrase your axioms so that they are not existential statements but rather operations. For example, define a union : Set → Set → Set operation and an axiom which states that u ε union X Y ↔ u ε X ∨ u ε Y. Formally, set theory does not have these operations, but every single development of set theory relies on the meta-theorem which says that introducing such constants is conservative (they can be eliminated). Also for the inductive set, introduce a constant S : Set and the axiom inductiveset S.

As a general advice, when formalizing mathematics in a proof assistants, one has to be quite flexible about organization of material. Traditional organization is good for teaching and writing textbooks, and so it may not align well with the demands of formalization.

For example, it looks to me at first sight that you would benefit by formalizing not only sets, but also classes. The class comprehension notation $\{ x \mid \phi(x) \}$ is very expressive and convenient, and easily formalized in terms of propositional functions on $\mathsf{Set}$. With it, you can define many operations on classes and then state that they are sets in terms of axioms. For example, rather than axiomatizing a union operation we just define union X Y to be the class {u | u ε X ∨ u ε Y} and then state that this class is a set. I suppose you could look at Von Neumann–Bernays–Gödel set theory.

StackExchange Computer Science Q#123837, answer score: 8