diff --git a/Mathlib/Order/Cofinal.lean b/Mathlib/Order/Cofinal.lean
index 0e8b480d90627f..ce94954545c4d6 100644
--- a/Mathlib/Order/Cofinal.lean
+++ b/Mathlib/Order/Cofinal.lean
@@ -17,11 +17,10 @@ import Mathlib.Data.Set.Lattice
 A set `s` in an ordered type `α` is cofinal when for every `a : α` there exists an element of `s`
 greater or equal to it. This file provides a basic API for the `IsCofinal` predicate.
 
-For the cofinality of a set as a cardinal, see `Mathlib/SetTheory/Cardinal/Cofinality.lean`.
+For the cofinality of a set as a cardinal, see `Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean`.
 
 ## TODO
 
-- Define `Order.cof` in terms of `Cofinal`.
 - Deprecate `Order.Cofinal` in favor of this predicate.
 -/