# Zulip Chat Archive

## Stream: new members

### Topic: pairs equal iff projections are?

#### Marcus Klaas (Dec 02 2018 at 12:50):

Can anyone give me a pointer on how prove this?

example {α β} {a c : α} {b d : β} (h: (a, b) = (c, d)) : a = c := sorry

#### Kevin Buzzard (Dec 02 2018 at 12:51):

example {α β} {a c : α} {b d : β} (h: (a, b) = (c, d)) : a = c := begin cases h, refl, end

#### Patrick Massot (Dec 02 2018 at 12:54):

The state after `cases`

is a bit weird. You can also directly provide the proof term `(prod.mk.inj h).left`

#### Kevin Buzzard (Dec 02 2018 at 12:54):

example {α β} {a c : α} {b d : β} (h: (a, b) = (c, d)) : a = c := (prod.mk.inj h).1

#### Marcus Klaas (Dec 02 2018 at 12:54):

Thanks so much!!

#### Kevin Buzzard (Dec 02 2018 at 12:55):

example {α β} : ∀ {a c : α} {b d : β} (h: (a, b) = (c, d)), a = c | a c b d rfl := rfl

#### Kevin Buzzard (Dec 02 2018 at 12:56):

So that's a tactic mode proof, a term mode proof, and a proof using the equation compiler.

#### Marcus Klaas (Dec 02 2018 at 12:58):

Haha, that's great :D - I'm not quite sure how the equation compiler does it tho ;p

#### Kevin Buzzard (Dec 02 2018 at 13:00):

`(a, b)`

has type `prod \alpha \beta`

, an inductive type, so you need tools to deal with terms of this type. When the inductive type `prod`

is defined, Lean creates with it its recursor `prod.rec`

, which is the universal way to define a map from `prod \alpha \beta`

to anywhere. Lean then creates a bunch of other useful functions automatically, you can see what they are by typing `#print prefix prod`

. There's usually something called `X.mk.inj`

in there for an inductive type `X`

, so that's what I was looking for. That's how I found the term proof. For the tactic mode proof, `cases`

is a great tactic for any inductive type, it takes the type to pieces.

For the equation compiler proof, we make Lean do the work. I had to move things to the other side of the colon. The point is that I can tell Lean that without loss of generality `h`

*must* be `rfl`

. I still don't really understand how the equation compiler actually works, but I have sort-of got the hang of how to use it in practice. Your question is a great basic example of how to use its power.

#### Mario Carneiro (Dec 02 2018 at 13:02):

it uses `prod.no_confusion`

under the hood, which is basically the same as `prod.inj`

#### Marcus Klaas (Dec 02 2018 at 13:03):

You folks are amazing. Thank you.

#### Kevin Buzzard (Dec 02 2018 at 13:04):

Just to be clear -- moving stuff to before or after the colon doesn't change the proposition, it's just a trick for controlling whether or not you have to give the inputs yourself in the "first line" of your proof.

Last updated: May 11 2021 at 14:11 UTC