feat: basic instances for ULift and PLift

src/Init/Data.lean

@@ -37,3 +37,5 @@ import Init.Data.Cast
 import Init.Data.Sum
 import Init.Data.BEq
 import Init.Data.Subtype
+import Init.Data.ULift
+import Init.Data.PLift

src/Init/Data/PLift.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Core
+
+deriving instance DecidableEq for PLift
+
+instance [Subsingleton α] : Subsingleton (PLift α) where
+  allEq := fun ⟨a⟩ ⟨b⟩ => congrArg PLift.up (Subsingleton.elim a b)

src/Init/Data/ULift.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Core
+
+deriving instance DecidableEq for ULift
+
+instance [Subsingleton α] : Subsingleton (ULift α) where
+  allEq := fun ⟨a⟩ ⟨b⟩ => congrArg ULift.up (Subsingleton.elim a b)