fix

Author: vihdzp

Mathlib/Order/DirSupClosed.lean

@@ -291,18 +291,14 @@ end Preorder
 section PartialOrder
 variable [PartialOrder α]
 
-theorem DirSupClosed.singleton (a : α) : DirSupClosed {a} := by
+theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by
   intro d hda hdn _ b hb
   rw [hdn.subset_singleton_iff] at hda
   subst hda
   exact mem_singleton_of_eq (hb.unique isLUB_singleton)
 
-@[deprecated (since := "2026-05-22")] alias dirSupClosed_singleton := DirSupClosed.singleton
-
-theorem DirSupClosedOn.singleton (a : α) : DirSupClosedOn D {a} :=
-  (DirSupClosed.singleton a).dirSupClosedOn
-
-@[deprecated (since := "2026-05-22")] alias dirSupClosedOn_singleton := DirSupClosedOn.singleton
+theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} :=
+  (dirSupClosed_singleton a).dirSupClosedOn
 
 end PartialOrder
 

Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean

@@ -131,9 +131,6 @@ theorem cof_congr_of_strictMono {f : α → γ} (hf : StrictMono f) (hf' : IsCof
     cof α = cof γ := by
   simpa using lift_cof_congr_of_strictMono hf hf'
 
-theorem cof_eq_of_isCofinal {s : Set α} (hs : IsCofinal s) : cof s = cof α :=
-  cof_congr_of_strictMono (Subtype.strictMono_coe _) (by simpa)
-
 @[simp]
 theorem cof_lt_aleph0_iff : Order.cof α < ℵ₀ ↔ Order.cof α ≤ 1 := by
   refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩