From e573676db1d078d1b6d83cec2f16c818ca3a5b96 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Mon, 4 Nov 2024 19:38:13 -0600
Subject: [PATCH] feat: `List.pmap_eq_self` (#5927)

This is a `pmap` analog of
[`List.map_id''`](https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Lemmas.html#List.map_id'').

As discussed on
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60pmap_eq_self.60/near/472496933).
---
 src/Init/Data/List/Attach.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 925ccdf55ee5..f0a07e025f4d 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -169,6 +169,13 @@ theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Li
     (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by
   simp
 
+theorem pmap_eq_self {l : List α} {p : α → Prop} (hp : ∀ (a : α), a ∈ l → p a)
+    (f : (a : α) → p a → α) : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a := by
+  rw [pmap_eq_map_attach]
+  conv => lhs; rhs; rw [← attach_map_subtype_val l]
+  rw [map_inj_left]
+  simp
+
 @[simp]
 theorem attach_eq_nil_iff {l : List α} : l.attach = [] ↔ l = [] :=
   pmap_eq_nil_iff