One-line proof

Stream: new members

[Bhavik Mehta]

What's the one-line proof that I'm missing:

example {α β : Type} {x : α} {y z : β} (h : (x, y) = (x, z)) : y = z :=
begin
  sorry -- simp [h]
end

[Bhavik Mehta]

I guess revert h, simp works...

[Mario Carneiro]

cases h; refl

[Rob Lewis]

Or injection h

[Bhavik Mehta]

Ah, injection is what I was looking for. I don't get what cases is doing in that line, and why that works

[Bhavik Mehta]

Out of interest, how would I prove this in term mode

[Marc Huisinga]

example {α β : Type} {x : α} {y z : β} (h : (x, y) = (x, z)) : y = z := (prod.mk.inj h).2

prod.mk.inj uses prod.no_confusion which afaik you get for all inductive types that are not propositions

[Andrew Ashworth]

yes, it's auto-generated afaik

example {α β : Type} {x : α} {y z : β} (h : (x, y) = (x, z)) : y = z := prod.no_confusion h (λ _, id)

[Chris B]

Yeah, no_confusion is what you want when you'd like to show that a constructor is injective and/or disjoint. The sources below have some more detailed info. FWIW no_confusion is defined in terms of another definition called no_confusion_type which I find easier on the eyes.

https://github.com/leanprover/tutorial/blob/master/06_Inductive_Types.org
https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

[Mario Carneiro]

Here's a proof directly from axioms:

example {α β : Type} {x : α} {y z : β} : (x, y) = (x, z) → y = z :=
@congr_arg _ β (x, y) (x, z) (@prod.rec _ β (λ _, β) (λ a b, b))

[Mario Carneiro]

or more simply

example {α β : Type} {x : α} {y z : β} : (x, y) = (x, z) → y = z :=
congr_arg prod.snd