## Stream: general

### Topic: And-elim phrasing

#### Patrick Stevens (May 28 2018 at 19:33):

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 (May 28 2018 at 19:33):

cases h with hp hq

cases

#### Patrick Massot (May 28 2018 at 19:33):

almost fast enough!

#### Patrick Massot (May 28 2018 at 19:34):

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

#### Patrick Stevens (May 28 2018 at 19:34):

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

#### Patrick Massot (May 28 2018 at 19:34):

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

#### Patrick Massot (May 28 2018 at 19:35):

Not trivial to find, I agree

#### Patrick Massot (May 28 2018 at 19:35):

But very important reading

#### Reid Barton (May 28 2018 at 19:35):

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

#### Kevin Buzzard (May 28 2018 at 21:42):

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

Last updated: May 10 2021 at 00:31 UTC