Does Lean have definitorial expansion?

Stream: general

[Fames Yasd]

So let's suppose I have proved a theorem: exists! x, P x. can I now define this 'x' as 'c' and have two theorems:
P c and forall y, P y -> y = c? The same thing with functions, if I proved forall A,B exists! C P(C) can I now define a function symbol 'f' such that
forall A B, P(f(A,B)).

[Kenny Lau]

that isn't "definitorial expansion"

[Kenny Lau]

you can use classical.some (and its friend classical.some_spec)