Comment by sanxiyn

Lean's three standard axioms are documented in The Lean Language Reference.

https://lean-lang.org/doc/reference/latest/Axioms/#standard-...

The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → α

The axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = b

The quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b)