How to prove r → (∃ x : α, r) in Lean

Question

I'm trying to prove the logical statement r → (∃ x : α, r), where r is a Prop (a proposition or statement) and α 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 α being uninhabited make this a false statement since no x of type α exists?

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 α, 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

  ¬ (∃ x : α, r) → (∀ x : α, ¬ r) → ??

I'm not sure how to perform that first implication in lean, and even if I did, I would still need an x of type α to eliminate the ∀.

Any hints would be appreciated.

Answer 1

That statement isn't true in general. α could be empty:

example : ¬ ∀ (α : Type) (r : Prop), r → (∃ x : α, r) :=
begin
  intro h,
  cases h empty _ true.intro with w,
  cases w
end

You can prove the original statement if you assume [inhabited α]

example (α : Type) [inhabited α] (r : Prop) : r → (∃ x : α, r) :=
λ h, ⟨inhabited.default α, h⟩