From c6cad5fcff86c6c9ee738bf4faaf643924c587ea Mon Sep 17 00:00:00 2001
From: user202729 <25191436+user202729@users.noreply.github.com>
Date: Sun, 1 Jun 2025 13:25:52 +0700
Subject: [PATCH] doc: fix a typo in ULift's documentation (#8571)

Just a typo. From my understanding (and the specification otherwise) the
resulting level is the maximum of `r` and `s` instead of the minimum.

No issue opened yet (thus the draft).
---
 src/Init/Prelude.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index d7fe4d774f..c204bebb3a 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -861,7 +861,7 @@ instance : Inhabited NonemptyType.{u} where
 Lifts a type to a higher universe level.
 
 `ULift α` wraps a value of type `α`. Instead of occupying the same universe as `α`, which would be
-the minimal level, it takes a further level parameter and occupies their minimum. The resulting type
+the minimal level, it takes a further level parameter and occupies their maximum. The resulting type
 may occupy any universe that's at least as large as that of `α`.
 
 The resulting universe of the lifting operator is the first parameter, and may be written explicitly