f : α × β → γ injective implies fun x ↦ f (a, x) injective

Stream: Is there code for X?

[David Renshaw]

I feel like there ought to be an existing lemma that does this

def foo {α β γ : Type} (f : α × β → γ) (hf : f.Injective) (a : α) :
    Function.Injective (fun x ↦ f (a, x)) := by
  intro a b hab
  have h1 := hf hab
  rw [Prod.mk.injEq] at h1
  exact h1.2

[Eric Rodriguez]

I don't think this already exists, by a Loogle feature I'm surprised works:

@loogle Function.Injective (α := Prod _ _)

[loogle]

:search: Function.Injective2.uncurry, Prod.fst_injective, and 24 more

[Eric Rodriguez]

None of the hits work; Injective2.uncurry seems to be the closest. I think there is a spelling for fun x ↦ f (a, x), no?

[Mauricio Collares]

It's also close to docs#Function.Injective2.right applied to curry f, but one needs to convert it back to the uncurried version using the function Eric mentioned.

[David Renshaw]

Oh, interesting. I was not aware of Injective2

[Eric Wieser]

Isn't this composition with the fact that prod.mk is injective?

[Anatole Dedecker]

Indeed I think the best way is to use docs#Prod.mk.inj_left