Existential Quantifier Elimination

Stream: new members

[Bolton Bailey]

Hello. I'm trying to prove a statement and among the givens is an existentially quantified proposition. My tactic state looks something like
h2 : \exists (a : A) (H : a \in my_finset), foo bar = a

I would like to get this into something like
a : A
H : a \in my_finset
h3 : foo bar = a

I sort of assumed this page https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html would explain how to accomplish this, but none of the snippets I found there work. Does anyone have any advice on how to do this/a better reference?

[Bryan Gin-ge Chen]

You can use tactic#rcases or tactic#obtain:

import tactic

example (A B : Type) (my_finset : finset A) (bar : B) (foo : B → A)
  (h2 : ∃ (a : A) (H : a ∈ my_finset), foo bar = a) : true :=
begin
  rcases h2 with ⟨a : A, H : a ∈ my_finset, h3 : foo bar = a⟩,
  -- type ascriptions are optional
  -- rcases h2 with ⟨a, H, h3⟩,
  sorry
end

example (A B : Type) (my_finset : finset A) (bar : B) (foo : B → A)
  (h2 : ∃ (a : A) (H : a ∈ my_finset), foo bar = a) : true :=
begin
  obtain ⟨a : A, H : a ∈ my_finset, h3 : foo bar = a⟩ := h2,
  -- type ascriptions are optional
  -- obtain ⟨a, H, h3⟩ := h2,
  sorry
end

[Bolton Bailey]

Yes, this works, thanks so much for your help

[Bryan Gin-ge Chen]

No problem! By the way, if you're using a recent version of Lean, hovering over the ∃ symbol should pop up some advice on how to prove an existential goal and how to use an existential hypothesis.