Intro Lean question

Stream: new members

[Kristaps John Balodis]

I'm just working my way through the start of Theorem Proving in Lean, and at the start of section 2.3 for

constant p : nat

it's claimed that

fst p : nat

but when I try

#check fst p

Lean doesn't like thefst. I tried some obvious things like *first * or 1st, but I'm not sure what command I should be using to refer to the first coordinate of p.

P.S. where/what is the best way to look this up so I don't have to post these basic questions here?

[Yakov Pechersky]

You need to have p : nat × nat

[Yakov Pechersky]

Otherwise, you just have a single nat, not a cartesian product.

[Yakov Pechersky]

image.png

[Kristaps John Balodis]

Ah sorry, that was a typo, I did have p :nat nat in the code. It still wasn't working, but I just figured out that either p.1 and p.fst both work. Thanks!

[Yakov Pechersky]

You can also open prod to get access to fst without having to write prod.fst