Stream: new members

Topic: Existential Quantifier Elimination

Bolton Bailey (Nov 18 2020 at 04:01):

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 (Nov 18 2020 at 04:06):

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 (Nov 18 2020 at 04:13):

Yes, this works, thanks so much for your help

Bryan Gin-ge Chen (Nov 18 2020 at 04:15):

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.

Last updated: Dec 20 2023 at 11:08 UTC