feat(Data/Part): Part.mem_right_unique (#24006)

Add the lemmas `Part.mem_right_unique` and `Part.Mem.right_unique`.



Co-authored-by: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>

Author: LorenzoLuccioli

Mathlib/Data/Part.lean

@@ -128,9 +128,15 @@ theorem some_dom (a : α) : (some a).Dom :=
 theorem mem_unique : ∀ {a b : α} {o : Part α}, a ∈ o → b ∈ o → a = b
   | _, _, ⟨_, _⟩, ⟨_, rfl⟩, ⟨_, rfl⟩ => rfl
 
+theorem mem_right_unique : ∀ {a : α} {o p : Part α}, a ∈ o → a ∈ p → o = p
+  | _, _, _, ⟨ho, _⟩, ⟨hp, _⟩ => ext' (iff_of_true ho hp) (by simp [*])
+
 theorem Mem.left_unique : Relator.LeftUnique ((· ∈ ·) : α → Part α → Prop) := fun _ _ _ =>
   mem_unique
 
+theorem Mem.right_unique : Relator.RightUnique ((· ∈ ·) : α → Part α → Prop) := fun _ _ _ =>
+  mem_right_unique
+
 theorem get_eq_of_mem {o : Part α} {a} (h : a ∈ o) (h') : get o h' = a :=
   mem_unique ⟨_, rfl⟩ h