In Lean, how do you prove a proposition of the form ∃ x : A, PP x ?

Question

In Lean, how do you prove a proposition of the form  ∃  x : A, PP x ?

Accepted Answer

Use the "existsi" tactic to provide a specific element a : A for which PP a holds.

Answer

Use the "cases" tactic to decompose the existential quantifier.

Answer

Use the "have" tactic to introduce a contradiction.

Answer

Use the "apply" tactic with an assumption of type  ∃  x : A, PP x.

Crowdly