## 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


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