I'm trying to prove the logical statement $r \implies (\exists x: \alpha, r)$, where $r$ is a Prop (a proposition or statement) and $\alpha$ is a Type. I've proved a few things in Lean, going through the exercises of the book, but I'm stuck on this one.
I'm really not sure I even understand why this is true. Wouldn't $\alpha$ being uninhabited make this a false statement since there does not exist $x \in \alpha$?
My best "attempts" were 1) hoping that lean's elaborator would fill in what I needed,
theorem t5_2: r → (∃ x : α, r) :=
assume rx: r,
⟨_, rx⟩
but it can't deduce something of type $\alpha$, which makes sense. And 2) I also thought that this might be a non-constructive proof, so I was thinking of doing a proof by contradiction. However, the furthest I got on paper was \begin{align} \lnot (\exists x \in \alpha, r) \implies (\forall x \in \alpha, \lnot r) \implies ?? \end{align} I'm not sure how to perform that first implication in lean, and even if I did, I would still need an $x \in \alpha$ to eliminate the $\forall$.
Any hints would be appreciated.