Does Lean4 provide contraposition in somewhere?

Stream: Is there code for X?

[Erika Su]

In Classical the em and dne (as byContradiction) are provided. Does the std provide contraposition and classical conversion for quantifier (Not ((x: X) -> P x)) -> Exist X (Not P) somewhere? Or are there some tactics serve the same purpose?