Extracting the value from a definition

Stream: new members

[Harun Khan]

In the context of a proof, what's another way of doing this:

have ⟨p, hp⟩: ∃ (p : Prop), p = True := sorry

I want to basically define p and extract hp : p = True.
I could instead do let p := True but then how would I get hp?

[Yaël Dillies]

set p := True with hp

[Harun Khan]

Is there a non-Mathlib way of doing it?

[Yaël Dillies]

let p := True
have hp : p = True := rfl

[Harun Khan]

I see. Yeah that's what I expected. Thanks.