And-elim phrasing

Stream: general

[Patrick Stevens]

Noob question here, trying to improve my mental model of Lean.
I have an inhabitant h of "and p q" in scope, and I want to create named inhabitants hp, hq of p and q respectively. I'm in tactic mode. One way to do this is "have hp : p, from h.left"; is that the one true way? Are there any other ways (that aren't just interchanging "and.left h" or "and.elim_left")?

[Reid Barton]

cases h with hp hq

[Patrick Massot]

cases

[Patrick Massot]

almost fast enough!

[Patrick Massot]

It's unfair, I was staring at an infinite class resolution trace when the notification popped up

[Patrick Stevens]

Thanks - it's nontrivial to search for this kind of thing in the docs

[Patrick Massot]

https://leanprover.github.io/theorem_proving_in_lean/tactics.html#more-tactics

[Patrick Massot]

Not trivial to find, I agree

[Patrick Massot]

But very important reading

[Reid Barton]

Yeah, I recommend a few rounds of reading that chapter and then playing around with stuff

[Kevin Buzzard]

We're trying to write docs, they appear in random places, but theorem proving in lean is where most of us started