instantiating existentials

Stream: general

[Hunter Freyer]

If I have a hypothesis h : \exists (a : A) (b : B), (P a b), how do I get a b and P a b into the context? cases h works kinda, but it plucks off the arguments one at a time and loses their parameter names.

[Heather Macbeth]

obtain ⟨a, b, hP⟩ := h

[Hunter Freyer]

phew, alright! Thanks! How does one find out about these tactics without harassing you helpful people??

[Sebastien Gouezel]

https://leanprover-community.github.io/mathlib_docs/tactics.html#obtain

[Patrick Massot]

Hunter, did you explore this webpage?

[Hunter Freyer]

Some of it, yes, but it's a bit of a "kitchen sink" of docs so it's hard to know how deep to dig into each doc...

[Hunter Freyer]

I hadn't seen the mathlib tactics docs, that should be helpful.

[Patrick Massot]

The answer to your question is in the tutorial project for instance.

[Hunter Freyer]

aha, I'd sort of glossed over that because it takes a very number-theory/equality-based style, when I'm doing more of a dependent-types/inductive-data style, so last time I looked it wasn't so useful. But I should remember to consult that again in the future

[Patrick Massot]

Number theory? @Kevin Buzzard did you read that?

[Patrick Massot]

Anyway, you seem to be a computer scientist, so the good resource for your is probably https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf

[Kevin Buzzard]

all that topological ring theory must have converted you