Lean prover: prove existential quantifier by providing an example

Question

I am a beginner in lean prover and I have struggled a bit with the following example:

I need to proof the following

∃ x, f x

Where f is a function defined earlier in the lean file. This seems simple enough and I can easily provide a proof in english (at least I think this is correct):

1. construct an arbitrary y such that f y holds.
2. By constructing an arbitrary y for which f y holds, we have proven the goal ∃ x, f x

However, translating this to lean gives me some problems. I tried using the "let" keyword to construct some arbitrary y for which f holds, but I then am unsure how to use this y to proof my goal

∃ x, f x

Is my thinking correct? How do I tackle this problem?

Answer 1

In Lean, the type Exists is defined as an inductive type as below:

inductive Exists {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists

So try either writing refine Exists.intro y _, (if in tactic mode) or let y := ... in Exists.intro _ (if in term mode) and seeing what the _ requires.

Answer 2

Using tactic mode:

lemma testproof : ∃ x : nat, x > 5 :=
begin
  apply exists.intro 6,
  dec_trivial,
end

#check testproof  -- testproof : ∃ (x : ℕ), x > 5

Using Exists directly (with @ to pass the arguments that would otherwise be inferred):

def testproof' := @Exists.intro nat (λ x, x > 5) 6 dec_trivial

#check testproof'  -- testproof' : ∃ (x : ℕ), x > 5