Combining 2 `List.map`s

Stream: Is there code for X?

[Snir Broshi]

import Mathlib
theorem foo {α β : Type*} {l₁ l₂ : List (α × β)}
    (h₁ : l₁.map Prod.fst = l₂.map Prod.fst)
    (h₂ : l₁.map Prod.snd = l₂.map Prod.snd) : l₁ = l₂ := by
  sorry

I think the strategy would be to first get l₁.map f = l₂.map f where f = fun p ↦ Prod.mk (Prod.fst p) (Prod.snd p) and then claim f = id.
This "combining 2 maps" thing surely already exists, but I couldn't find it.

[Markus Himmel]

How about this:

import Mathlib

theorem List.unzip_inj {α β : Type*} {l₁ l₂ : List (α × β)} :
    l₁.unzip = l₂.unzip ↔ l₁ = l₂ := by
  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
  rw [← zip_unzip l₁, ← zip_unzip l₂, h]

theorem foo {α β : Type*} {l₁ l₂ : List (α × β)}
    (h₁ : l₁.map Prod.fst = l₂.map Prod.fst)
    (h₂ : l₁.map Prod.snd = l₂.map Prod.snd) : l₁ = l₂ := by
  rw [← List.unzip_inj, List.unzip_eq_map, List.unzip_eq_map, h₁, h₂]

[Snir Broshi]

Cool, thanks!
List.unzip is useful in this case, but is there a general function to combine two lists with map?
Found it: docs#List.map₂Left and docs#List.map₂Right. I wonder if they can help here, though they seem to have very little API
docs#List.zipWith is probably the general way to combine two maps

[Snir Broshi]

Some version of this is now #32106