From 0a8d1bf808ec71aa685697b6ca9621f7f052b847 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 21 Aug 2024 21:37:13 +1000
Subject: [PATCH] feat: basic instances for ULift and PLift (#5112)

---
 src/Init/Data.lean       |  2 ++
 src/Init/Data/PLift.lean | 12 ++++++++++++
 src/Init/Data/ULift.lean | 12 ++++++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 src/Init/Data/PLift.lean
 create mode 100644 src/Init/Data/ULift.lean

diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index 91938d7707e1..8aceacd4189d 100644
--- a/src/Init/Data.lean
+++ b/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
diff --git a/src/Init/Data/PLift.lean b/src/Init/Data/PLift.lean
new file mode 100644
index 000000000000..d03ab7ccda6f
--- /dev/null
+++ b/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)
diff --git a/src/Init/Data/ULift.lean b/src/Init/Data/ULift.lean
new file mode 100644
index 000000000000..91276ebfea80
--- /dev/null
+++ 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)