diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index b974b8b6d0361..38b6c2e8fd865 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -1181,6 +1181,7 @@ set_option linter.deprecated false in
 theorem sup_le_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : sup.{_, v} f ≤ a ↔ ∀ i, f i ≤ a :=
   Ordinal.iSup_le_iff
 
+/-- `ciSup_le'` whenever the input type is small in the output universe. -/
 protected theorem iSup_le {ι} {f : ι → Ordinal.{u}} {a} :
     (∀ i, f i ≤ a) → iSup f ≤ a :=
   ciSup_le'
diff --git a/Mathlib/SetTheory/Ordinal/FixedPoint.lean b/Mathlib/SetTheory/Ordinal/FixedPoint.lean
index 2e5804f50bae6..c736f2c8641be 100644
--- a/Mathlib/SetTheory/Ordinal/FixedPoint.lean
+++ b/Mathlib/SetTheory/Ordinal/FixedPoint.lean
@@ -5,7 +5,6 @@ Authors: Violeta Hernández Palacios, Mario Carneiro
 -/
 import Mathlib.SetTheory.Ordinal.Enum
 import Mathlib.SetTheory.Ordinal.Exponential
-import Mathlib.Logic.UnivLE
 
 /-!
 # Fixed points of normal functions