feat(Data/List/Basic): bijectivity of List.map (#8642)

This adds `Function.{LeftInverse,RightInverse,Involutive,Surjective,Bijective}.list_map`, and corresponding `iff` lemmas.

`List.map_injective_iff` already existed, but has been golfed. The rest are new.

Mathlib/Data/List/Basic.lean

@@ -1765,20 +1765,6 @@ theorem map_eq_map {α β} (f : α → β) (l : List α) : f <$> l = map f l :=
 theorem map_tail (f : α → β) (l) : map f (tail l) = tail (map f l) := by cases l <;> rfl
 #align list.map_tail List.map_tail
 
-@[simp]
-theorem map_injective_iff {f : α → β} : Injective (map f) ↔ Injective f := by
-  constructor <;> intro h x y hxy
-  · suffices [x] = [y] by simpa using this
-    apply h
-    simp [hxy]
-  · induction' y with yh yt y_ih generalizing x
-    · simpa using hxy
-    cases x
-    · simp at hxy
-    · simp only [map, cons.injEq] at hxy
-      simp [y_ih hxy.2, h hxy.1]
-#align list.map_injective_iff List.map_injective_iff
-
 /-- A single `List.map` of a composition of functions is equal to
 composing a `List.map` with another `List.map`, fully applied.
 This is the reverse direction of `List.map_map`.
@@ -1795,6 +1781,68 @@ theorem map_comp_map (g : β → γ) (f : α → β) : map g ∘ map f = map (g
   ext l; rw [comp_map, Function.comp_apply]
 #align list.map_comp_map List.map_comp_map
 
+section map_bijectivity
+
+theorem _root_.Function.LeftInverse.list_map {f : α → β} {g : β → α} (h : LeftInverse f g) :
+    LeftInverse (map f) (map g)
+  | [] => by simp_rw [map_nil]
+  | x :: xs => by simp_rw [map_cons, h x, h.list_map xs]
+
+nonrec theorem _root_.Function.RightInverse.list_map {f : α → β} {g : β → α}
+    (h : RightInverse f g) : RightInverse (map f) (map g) :=
+  h.list_map
+
+nonrec theorem _root_.Function.Involutive.list_map {f : α → α}
+    (h : Involutive f) : Involutive (map f) :=
+  Function.LeftInverse.list_map h
+
+@[simp]
+theorem map_leftInverse_iff {f : α → β} {g : β → α} :
+    LeftInverse (map f) (map g) ↔ LeftInverse f g :=
+  ⟨fun h x => by injection h [x], (·.list_map)⟩
+
+@[simp]
+theorem map_rightInverse_iff {f : α → β} {g : β → α} :
+    RightInverse (map f) (map g) ↔ RightInverse f g := map_leftInverse_iff
+
+@[simp]
+theorem map_involutive_iff {f : α → α} :
+    Involutive (map f) ↔ Involutive f := map_leftInverse_iff
+
+theorem _root_.Function.Injective.list_map {f : α → β} (h : Injective f) :
+    Injective (map f)
+  | [], [], _ => rfl
+  | x :: xs, y :: ys, hxy => by
+    injection hxy with hxy hxys
+    rw [h hxy, h.list_map hxys]
+
+@[simp]
+theorem map_injective_iff {f : α → β} : Injective (map f) ↔ Injective f := by
+  refine ⟨fun h x y hxy => ?_, (·.list_map)⟩
+  suffices [x] = [y] by simpa using this
+  apply h
+  simp [hxy]
+#align list.map_injective_iff List.map_injective_iff
+
+theorem _root_.Function.Surjective.list_map {f : α → β} (h : Surjective f) :
+    Surjective (map f) :=
+  let ⟨_, h⟩ := h.hasRightInverse; h.list_map.surjective
+
+@[simp]
+theorem map_surjective_iff {f : α → β} : Surjective (map f) ↔ Surjective f := by
+  refine ⟨fun h x => ?_, (·.list_map)⟩
+  let ⟨[y], hxy⟩ := h [x]
+  exact ⟨_, List.singleton_injective hxy⟩
+
+theorem _root_.Function.Bijective.list_map {f : α → β} (h : Bijective f) : Bijective (map f) :=
+  ⟨h.1.list_map, h.2.list_map⟩
+
+@[simp]
+theorem map_bijective_iff {f : α → β} : Bijective (map f) ↔ Bijective f := by
+  simp_rw [Function.Bijective, map_injective_iff, map_surjective_iff]
+
+end map_bijectivity
+
 theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
     map f (filter p as) = foldr (fun a bs => bif p a then f a :: bs else bs) [] as := by
   induction' as with head tail