diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index 10ebaa481ad46..cfd91460ac93e 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -335,14 +335,14 @@ def liftInitialSeg : Cardinal.{u} ≤i Cardinal.{max u v} := by
     rintro ⟨a, ⟨b, rfl⟩⟩
     exact ⟨b, rfl⟩
 
-theorem mem_range_of_le_lift {a : Cardinal.{u}} {b : Cardinal.{max u v}} :
+theorem mem_range_lift_of_le {a : Cardinal.{u}} {b : Cardinal.{max u v}} :
     b ≤ lift.{v, u} a → b ∈ Set.range lift.{v, u} :=
   liftInitialSeg.mem_range_of_le
 
-@[deprecated mem_range_of_le_lift (since := "2024-10-07")]
+@[deprecated mem_range_lift_of_le (since := "2024-10-07")]
 theorem lift_down {a : Cardinal.{u}} {b : Cardinal.{max u v}} :
     b ≤ lift.{v, u} a → ∃ a', lift.{v, u} a' = b :=
-  mem_range_of_le_lift
+  mem_range_lift_of_le
 
 /-- `Cardinal.lift` as an `OrderEmbedding`. -/
 @[deprecated Cardinal.liftInitialSeg (since := "2024-10-07")]
@@ -1037,7 +1037,7 @@ theorem lift_sSup {s : Set Cardinal} (hs : BddAbove s) :
   apply ((le_csSup_iff' (bddAbove_image.{_,u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)
   · intro c hc
     by_contra h
-    obtain ⟨d, rfl⟩ := Cardinal.mem_range_of_le_lift (not_le.1 h).le
+    obtain ⟨d, rfl⟩ := Cardinal.mem_range_lift_of_le (not_le.1 h).le
     simp_rw [lift_le] at h hc
     rw [csSup_le_iff' hs] at h
     exact h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)
diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean
index e0ff450fad422..08369b5257281 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean
@@ -700,7 +700,7 @@ theorem cof_univ : cof univ.{u, v} = Cardinal.univ.{u, v} :=
       rcases @cof_eq Ordinal.{u} (· < ·) _ with ⟨S, H, Se⟩
       rw [univ, ← lift_cof, ← Cardinal.lift_lift.{u+1, v, u}, Cardinal.lift_lt, ← Se]
       refine lt_of_not_ge fun h => ?_
-      cases' Cardinal.mem_range_of_le_lift h with a e
+      cases' Cardinal.mem_range_lift_of_le h with a e
       refine Quotient.inductionOn a (fun α e => ?_) e
       cases' Quotient.exact e with f
       have f := Equiv.ulift.symm.trans f