diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean
index 7ecf948d2..b71be1ad3 100644
--- a/Manual/ErrorExplanations.lean
+++ b/Manual/ErrorExplanations.lean
@@ -7,6 +7,7 @@ Author: Joseph Rotella, Rob Simmons
 import Manual.Meta.ErrorExplanation
 import Manual.ErrorExplanations.CtorResultingTypeMismatch
 import Manual.ErrorExplanations.DependsOnNoncomputable
+import Manual.ErrorExplanations.HighInferredUniverse
 import Manual.ErrorExplanations.InductionWithNoAlts
 import Manual.ErrorExplanations.InductiveParamMismatch
 import Manual.ErrorExplanations.InductiveParamMissing
@@ -83,6 +84,8 @@ by Lean when processing a source file. All error names listed below have the
 
 {include 0 Manual.ErrorExplanations.DependsOnNoncomputable}
 
+{include 0 Manual.ErrorExplanations.HighInferredUniverse}
+
 {include 0 Manual.ErrorExplanations.InductionWithNoAlts}
 
 {include 0 Manual.ErrorExplanations.InductiveParamMismatch}
diff --git a/Manual/ErrorExplanations/HighInferredUniverse.lean b/Manual/ErrorExplanations/HighInferredUniverse.lean
new file mode 100644
index 000000000..786f5d340
--- /dev/null
+++ b/Manual/ErrorExplanations/HighInferredUniverse.lean
@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Rob Simmons, Kyle Miller
+-/
+
+import VersoManual
+import Manual.Meta.ErrorExplanation
+
+open Lean
+open Verso.Genre Manual InlineLean
+
+#doc (Manual) "About: `highInferredUniverse`" =>
+%%%
+shortTitle := "highInferredUniverse"
+%%%
+
+{errorExplanationHeader lean.highInferredUniverse}
+
+This error message appears when Lean's elaboration algorithm is about to assign a new type to a
+higher universe than may be necessary.
+
+::::paragraph
+Constructor argument universe levels must be no greater than the resulting universe level, so given
+this definition:
+:::keepEnv
+```lean
+inductive MaybeTwo (α : Type u)
+  | none
+  | some (fst snd : α)
+```
+```lean -show
+variable (α : Type u)
+```
+then the universe for {lean}`MaybeTwo α` must be {lean}`Type u` or higher.
+Lean automatically infers the universe to be the least universe, hence it chooses {lean}`Type u`, or, equivalently,
+{lean}`Sort (u + 1)`. (See the reference guide to {ref "universes-sorts"}[Universes] for more
+details on the relationship between {lean}`Prop`, {lean}`Sort`, and {lean}`Type`.)
+:::
+::::
+
+There are certain situations where universe inference yields a universe level that may be higher
+than it could be.
+In these situations, Lean chooses to avoid silently accepting this unnecessarily high universe
+level, because unnecessarily high universe levels can cause hard-to-diagnose errors in later
+definitions.
+Avoiding these situations requires an explicitly provided universe for the inductive type using a
+universe level in a slightly different form.
+This can't currently be done automatically, so fixing it requires user intervention.
+
+# Examples
+:::errorExample "Use of `Type` May Force Universe Too High"
+```broken
+structure MyPair (α β : Sort u) : Type _ where
+  (a : α)
+  (b : β)
+```
+
+```output
+Resulting type is of the form
+  Type ?u.6
+but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using
+  Sort (max 1 u)
+if the resulting universe level should be at the above universe level or higher.
+
+Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form `?u.6+1`. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s):
+  u ≤ ?u.6+1
+However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary.
+```
+
+```fixed "remove annotation"
+structure MyPair (α β : Sort u) where
+  (a : α)
+  (b : β)
+```
+
+```fixed "accept suggestion"
+structure MyPair (α β : Sort u) : Sort (max 1 u) where
+  (a : α)
+  (b : β)
+```
+
+```fixed "restrict arguments"
+structure MyPair (α β : Type u) : Type _ where
+  (a : α)
+  (b : β)
+```
+
+```fixed "make large type explicit"
+structure MyPair (α β : Sort u) : Type u where
+  (a : α)
+  (b : β)
+```
+
+```lean -show
+variable (α : Type u)
+```
+
+The initial type annotation {lean}`Type _` forces `MyPair` into a universe that looks like
+{lean}`Sort (_ + 1)`, but the best universe for `MyPair` is {lean}`Sort (max u 1)`. (See the section
+on {ref "prop-vs-type"}[Prop vs Type] for why it is {lean}`Sort (max u 1)` and not just
+{lean}`Sort u`.)
+
+The first two fixes are all equivalent, and allow `MyPair` to have any non-zero universe that
+is larger than `u`. The last two fixes make `MyPair` less general, but also silence the error.
+:::
+
+:::errorExample "Inductive Definition Needs Sort Annotations"
+```broken
+inductive Bar
+| foobar {Foo} : Foo → Bar
+| barbar : Option Bar → Bar
+```
+```output
+Resulting type is of the form
+  Type ?u.16
+but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using
+  Type u_1
+if the resulting universe level should be at the above universe level or higher.
+
+Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form `?u.16+1`. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s):
+  u_1 ≤ ?u.16+1
+However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary.
+```
+```fixed
+inductive Bar : Type u
+| foobar {Foo : Sort u} : Foo → Bar
+| barbar : Option Bar → Bar
+```
+
+In this case, the error message is a false positive, but the issue can be easily fixed with
+clarifying annotations. After annotating Foo with a universe `u`, the overall type can be assigned
+type that the error message suggests, which silences the error.
+:::
diff --git a/Manual/Types.lean b/Manual/Types.lean
index 1c1b49ccb..011fb1992 100644
--- a/Manual/Types.lean
+++ b/Manual/Types.lean
@@ -170,6 +170,9 @@ Propositions have the following properties:
 {docstring propext}
 
 # Universes
+%%%
+tag := "universes-sorts"
+%%%
 
 Types are classified by {deftech}_universes_. {index}[universe]{margin}[Universes are also referred to as {deftech}_sorts_.]
 Each universe has a {deftech (key:="universe level")}_level_, {index (subterm := "of universe")}[level] which is a natural number.