From 9641a9ac6c05e522ae347a3fa291b0c0ae6468b9 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 25 Jun 2025 11:04:52 +0200
Subject: [PATCH] feat: PULift (#8992)

This PR adds `PULift`, a more general form of `ULift` and `PLift` that
subsumes both.

Needed in #8973
---
 src/Init/Core.lean    |  1 +
 src/Init/Prelude.lean | 21 +++++++++++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 864b7280e0..cb582692c0 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1592,6 +1592,7 @@ gen_injective_theorems% MProd
 gen_injective_theorems% NonScalar
 gen_injective_theorems% Option
 gen_injective_theorems% PLift
+gen_injective_theorems% PULift
 gen_injective_theorems% PNonScalar
 gen_injective_theorems% PProd
 gen_injective_theorems% Prod
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index ef0b40739d..16112b7b0b 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -890,6 +890,27 @@ theorem ULift.up_down {α : Type u} (b : ULift.{v} α) : Eq (up (down b)) b := r
 /-- Bijection between `α` and `ULift.{v} α` -/
 theorem ULift.down_up {α : Type u} (a : α) : Eq (down (up.{v} a)) a := rfl
 
+/--
+Lifts a type or proposition to a higher universe level.
+
+`PULift α` wraps a value of type `α`. It is a generalization of
+`PLift` that allows lifting values who's type may live in `Sort s`.
+It also subsumes `PLift`.
+-/
+-- The universe variable `r` is written first so that `ULift.{r} α` can be used
+-- when `s` can be inferred from the type of `α`.
+structure PULift.{r, s} (α : Sort s) : Sort (max s r 1) where
+  /-- Wraps a value to increase its type's universe level. -/
+  up ::
+  /-- Extracts a wrapped value from a universe-lifted type. -/
+  down : α
+
+/-- Bijection between `α` and `PULift.{v} α` -/
+theorem PULift.up_down {α : Sort u} (b : PULift.{v} α) : Eq (up (down b)) b := rfl
+
+/-- Bijection between `α` and `PULift.{v} α` -/
+theorem PULift.down_up {α : Sort u} (a : α) : Eq (down (up.{v} a)) a := rfl
+
 /--
 Either a proof that `p` is true or a proof that `p` is false. This is equivalent to a `Bool` paired
 with a proof that the `Bool` is `true` if and only if `p` is true.