inequality of prod constructor

Stream: Is there code for X?

[Eric Wieser]

Is there a nice way to show

example {α β} (a₁ a₂ : α) (b₁ b₂ : β) (h : a₁ ≠ a₂) : (a₁, b₁) ≠ (a₂, b₂) :=

[Eric Wieser]

λ h2, h $ by injection h2 works, but is a little annoying

[Yaël Dillies]

You can use function.injective.ne along with whichever injectivity lemma is needed here.

[Shing Tak Lam]

example {α β} (a₁ a₂ : α) (b₁ b₂ : β) (h : a₁ ≠ a₂) : (a₁, b₁) ≠ (a₂, b₂) :=
λ h₁, h (prod.mk.inj h₁).1

[Yaël Dillies]

So my solution should be (untested because I'm in the orange bar hell...)

example {α β} (a₁ a₂ : α) (b₁ b₂ : β) (h : a₁ ≠ a₂) : (a₁, b₁) ≠ (a₂, b₂) :=
prod.mk.inj_left.ne h

[Shing Tak Lam]

prod.mk.inj is not stated in terms of injective, it's

⊢ ∀ {α : Type u_1} {β : Type u_2} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β}, (x₁, y₁) = (x₂, y₂) → x₁ = x₂ ∧ y₁ = y₂

[Yaël Dillies]

Edited :grinning:

[Shing Tak Lam]

Still wrong :)

prod.mk.inj_left : ∀ {α : Type u_1} {β : Type u_2} (a : α), function.injective (prod.mk a)

(and inj_right isn't right either, since that assumes the second element of the tuples are the same, which in Eric's example it's not)

[Shing Tak Lam]

Shing Tak Lam said:

Still wrong :)

prod.mk.inj_left : ∀ {α : Type u_1} {β : Type u_2} (a : α), function.injective (prod.mk a)

(and inj_right isn't right either, since that assumes the second element of the tuples are the same, which in Eric's example it's not)

are the names of prod.mk.inj_(left|right)backwards? inj_left says it's injective on the second argument (while fixing the first), and inj_right says it's injective on the first argument (while fixing the second).

[Yaël Dillies]

Sounds like it, yeah.

[Adam Topaz]

example {α β} (a₁ a₂ : α) (b₁ b₂ : β) (h : a₁ ≠ a₂) : (a₁, b₁) ≠ (a₂, b₂) :=
λ c, h $ congr_arg prod.fst c

[Adam Topaz]

Or is that too low-level for your taste?