If have shown that a variable exsists how do I then use it.

Stream: lean4

[Timothy Harevy]

I have shown that there exists an N such that 1<e*N is true for all e in R and e>0 (Archmedian Property) but I now want to use this N that I have shown exists as a variable how do I now do this.

[Johan Commelin]

You can use the tactics obtain, rcases, or choose to destruct an existential into a witness and its property.