chore: deprecate Ordinal.blsub (leanprover-community#37064)

In favor of simply writing `⨆ i : Iio a, f i + 1`. See leanprover-community#17033.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: vihdzp

Mathlib/Order/InitialSeg.lean

@@ -288,6 +288,9 @@ theorem coe_fn_mk (f : r ↪r s) (t o) : (@PrincipalSeg.mk _ _ r s f t o : α 
 theorem mem_range_iff_rel (f : r ≺i s) : ∀ {b : β}, b ∈ Set.range f ↔ s b f.top :=
   f.mem_range_iff_rel' _
 
+theorem range_eq (f : r ≺i s) : Set.range f = {b | s b f.top} :=
+  Set.ext_iff.2 fun _ ↦ mem_range_iff_rel f
+
 theorem lt_top (f : r ≺i s) (a : α) : s (f a) f.top :=
   f.mem_range_iff_rel.1 ⟨_, rfl⟩
 
@@ -639,6 +642,9 @@ variable [PartialOrder β] {a a' : α} {b : β}
 theorem mem_range_of_le [LT α] (f : α <i β) (h : b ≤ f a) : b ∈ Set.range f :=
   (f : α ≤i β).mem_range_of_le h
 
+theorem range_eq_Iio [LT α] (f : α <i β) : Set.range f = Set.Iio f.top :=
+  f.range_eq
+
 theorem isLowerSet_range [LT α] (f : α <i β) : IsLowerSet (Set.range f) :=
   (f : α ≤i β).isLowerSet_range
 

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -506,14 +506,16 @@ theorem _root_.Cardinal.iSup_lt_of_lt_cof_ord {f : α → Cardinal.{u}} {a : Car
 
 -- TODO: use `⨆ i, f i + 1` instead of `lsub`
 
-private theorem card_mem_cof {o} : ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = o.card :=
-  ⟨_, _, lsub_typein o, mk_toType o⟩
-
 /-- The set in the `lsub` characterization of `cof` is nonempty. -/
+@[deprecated "to build an increasing function with limit o, use the fundamental sequence API."
+(since := "2026-03-27")]
 theorem cof_lsub_def_nonempty (o) :
     { a : Cardinal | ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a }.Nonempty :=
-  ⟨_, card_mem_cof⟩
+  ⟨_, ⟨_, _, lsub_typein o, mk_toType o⟩⟩
 
+set_option linter.deprecated false in
+@[deprecated "to build an increasing function with limit o, use the fundamental sequence API."
+(since := "2026-03-27")]
 theorem cof_eq_sInf_lsub (o : Ordinal.{u}) : cof o =
     sInf { a : Cardinal | ∃ (ι : Type u) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a } := by
   refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)
@@ -529,6 +531,9 @@ theorem cof_eq_sInf_lsub (o : Ordinal.{u}) : cof o =
     rw [← not_lt, ← typein_le_typein, typein_enum] at hb'
     exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)
 
+set_option linter.deprecated false in
+@[deprecated "to build an increasing function with limit o, use the fundamental sequence API."
+(since := "2026-03-27")]
 theorem exists_lsub_cof (o : Ordinal) :
     ∃ (ι : _) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = cof o := by
   rw [cof_eq_sInf_lsub]
@@ -544,6 +549,7 @@ theorem cof_lsub_le_lift {ι} (f : ι → Ordinal) :
   rw [← lift_id'.{u} (lsub f), ← Cardinal.lift_umax.{u, v}]
   exact cof_lift_iSup_add_one_le _
 
+set_option linter.deprecated false in
 @[deprecated le_cof_iff (since := "2026-03-21")]
 theorem le_cof_iff_lsub {o : Ordinal} {a : Cardinal} :
     a ≤ cof o ↔ ∀ {ι} (f : ι → Ordinal), lsub.{u, u} f = o → a ≤ #ι := by
@@ -618,6 +624,7 @@ theorem nfp_lt_ord {f : Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hf : ∀
     a < c → nfp f a < c :=
   nfpFamily_lt_ord_lift hc (by simpa using Cardinal.one_lt_aleph0.trans hc) fun _ => hf
 
+set_option linter.deprecated false in
 @[deprecated exists_lsub_cof (since := "2026-03-21")]
 theorem exists_blsub_cof (o : Ordinal) :
     ∃ f : ∀ a < (cof o).ord, Ordinal, blsub.{u, u} _ f = o := by

Mathlib/SetTheory/Ordinal/Family.lean

@@ -632,13 +632,9 @@ theorem iSup_typein_limit {o : Ordinal.{u}} (ho : ∀ a, a < o → succ a < o) :
 @[simp]
 theorem iSup_typein_succ {o : Ordinal} :
     iSup (typein ((· < ·) : (succ o).ToType → (succ o).ToType → Prop)) = o := by
-  rcases iSup_eq_lsub_or_succ_iSup_eq_lsub
-      (typein ((· < ·) : (succ o).ToType → (succ o).ToType → Prop)) with h | h
-  · rw [iSup_eq_lsub_iff] at h
-    simp only [lsub_typein] at h
-    exact (h o (lt_succ o)).false.elim
-  rw [← succ_eq_succ_iff, h]
-  apply lsub_typein
+  rw [← csSup_Iic (a := o), iSup, PrincipalSeg.range_eq]
+  congr
+  simp
 
 @[deprecated (since := "2025-10-01")] alias sup_eq_lsub := iSup_eq_lsub
 @[deprecated (since := "2025-10-01")] alias sup_le_lsub := iSup_le_lsub
@@ -654,87 +650,110 @@ theorem iSup_typein_succ {o : Ordinal} :
 
 end lsub
 
--- TODO: either deprecate this in favor of `lsub` when its universes are generalized, or deprecate
--- both of them at once.
-
 section blsub
 
 /-- The least strict upper bound of a family of ordinals indexed by the set of ordinals less than
-    some `o : Ordinal.{u}`.
-
-    This is to `lsub` as `bsup` is to `sup`. -/
+some `o : Ordinal.{u}`. -/
+@[deprecated "write `⨆ i : Iio o, f i + 1` instead." (since := "2026-03-23")]
 def blsub (o : Ordinal.{u}) (f : ∀ a < o, Ordinal.{max u v}) : Ordinal.{max u v} :=
   bsup.{_, v} o fun a ha => succ (f a ha)
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_eq_blsub (o : Ordinal.{u}) (f : ∀ a < o, Ordinal.{max u v}) :
     (bsup.{_, v} o fun a ha => succ (f a ha)) = blsub.{_, v} o f :=
   rfl
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem lsub_eq_blsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} (ho : type r = o)
     (f : ∀ a < o, Ordinal) : lsub (familyOfBFamily' r ho f) = blsub o f :=
   iSup'_eq_bsup r ho fun a ha => succ (f a ha)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem lsub_eq_lsub {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r]
     [IsWellOrder ι' r'] {o} (ho : type r = o) (ho' : type r' = o)
     (f : ∀ a < o, Ordinal.{max u v}) :
     lsub.{_, v} (familyOfBFamily' r ho f) = lsub.{_, v} (familyOfBFamily' r' ho' f) := by
   rw [lsub_eq_blsub', lsub_eq_blsub']
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem lsub_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     lsub.{_, v} (familyOfBFamily o f) = blsub.{_, v} o f :=
   lsub_eq_blsub' _ _ _
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_eq_lsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r]
     (f : ι → Ordinal.{max u v}) : blsub.{_, v} _ (bfamilyOfFamily' r f) = lsub.{_, v} f :=
   bsup'_eq_iSup r (succ ∘ f)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_eq_blsub {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r']
     (f : ι → Ordinal.{max u v}) :
     blsub.{_, v} _ (bfamilyOfFamily' r f) = blsub.{_, v} _ (bfamilyOfFamily' r' f) := by
   rw [blsub_eq_lsub', blsub_eq_lsub']
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) :
     blsub.{_, v} _ (bfamilyOfFamily f) = lsub.{_, v} f :=
   blsub_eq_lsub' _ _
 
-@[congr]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_congr {o₁ o₂ : Ordinal.{u}} (f : ∀ a < o₁, Ordinal.{max u v}) (ho : o₁ = o₂) :
     blsub.{_, v} o₁ f = blsub.{_, v} o₂ fun a h => f a (h.trans_eq ho.symm) := by
   subst ho
   rfl
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_le_iff {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}} {a} :
     blsub.{_, v} o f ≤ a ↔ ∀ i h, f i h < a := by
   convert bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2
   simp_rw [succ_le_iff]
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_le {o : Ordinal} {f : ∀ b < o, Ordinal} {a} : (∀ i h, f i h < a) → blsub o f ≤ a :=
   blsub_le_iff.2
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem lt_blsub {o} (f : ∀ a < o, Ordinal) (i h) : f i h < blsub o f :=
   blsub_le_iff.1 le_rfl _ _
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem lt_blsub_iff {o : Ordinal.{u}} {f : ∀ b < o, Ordinal.{max u v}} {a} :
     a < blsub.{_, v} o f ↔ ∃ i hi, a ≤ f i hi := by
   simpa only [not_forall, not_lt, not_le] using not_congr (@blsub_le_iff.{_, v} _ f a)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     bsup.{_, v} o f ≤ blsub.{_, v} o f :=
   bsup_le fun i h => (lt_blsub f i h).le
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_le_bsup_succ {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     blsub.{_, v} o f ≤ succ (bsup.{_, v} o f) :=
   blsub_le fun i h => lt_succ_iff.2 (le_bsup f i h)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     bsup.{_, v} o f = blsub.{_, v} o f ∨ succ (bsup.{_, v} o f) = blsub.{_, v} o f := by
   rw [← iSup_eq_bsup, ← lsub_eq_blsub]
   exact iSup_eq_lsub_or_succ_iSup_eq_lsub _
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_succ_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     succ (bsup.{_, v} o f) ≤ blsub.{_, v} o f ↔ ∃ i hi, f i hi = bsup.{_, v} o f := by
   refine ⟨fun h => ?_, ?_⟩
@@ -746,58 +765,78 @@ theorem bsup_succ_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v})
   rw [succ_le_iff, ← hf]
   exact lt_blsub _ _ _
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_succ_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     succ (bsup.{_, v} o f) = blsub.{_, v} o f ↔ ∃ i hi, f i hi = bsup.{_, v} o f :=
   (blsub_le_bsup_succ f).ge_iff_eq'.symm.trans (bsup_succ_le_blsub f)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_eq_blsub_iff_succ {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     bsup.{_, v} o f = blsub.{_, v} o f ↔ ∀ a < blsub.{_, v} o f, succ a < blsub.{_, v} o f := by
   rw [← iSup_eq_bsup, ← lsub_eq_blsub]
   apply iSup_eq_lsub_iff
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_eq_blsub_iff_lt_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
     bsup.{_, v} o f = blsub.{_, v} o f ↔ ∀ i hi, f i hi < bsup.{_, v} o f :=
   ⟨fun h i => by
     rw [h]
     apply lt_blsub, fun h => le_antisymm (bsup_le_blsub f) (blsub_le h)⟩
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : IsSuccLimit o)
     {f : ∀ a < o, Ordinal.{max u v}} (hf : ∀ a ha, f a ha < f (succ a) (ho.succ_lt ha)) :
     bsup.{_, v} o f = blsub.{_, v} o f := by
   rw [bsup_eq_blsub_iff_lt_bsup]
   exact fun i hi => (hf i hi).trans_le (le_bsup f _ _)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_succ_of_mono {o : Ordinal.{u}} {f : ∀ a < succ o, Ordinal.{max u v}}
     (hf : ∀ {i j} (hi hj), i ≤ j → f i hi ≤ f j hj) : blsub.{_, v} _ f = succ (f o (lt_succ o)) :=
   bsup_succ_of_mono fun {_ _} hi hj h => succ_le_succ (hf hi hj h)
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_eq_zero_iff {o} {f : ∀ a < o, Ordinal} : blsub o f = 0 ↔ o = 0 := by
   rw [← lsub_eq_blsub, lsub_eq_zero_iff]
   exact isEmpty_toType_iff
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_zero (f : ∀ a < (0 : Ordinal), Ordinal) : blsub 0 f = 0 := by rw [blsub_eq_zero_iff]
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_pos {o : Ordinal} (ho : 0 < o) (f : ∀ a < o, Ordinal) : 0 < blsub o f :=
   (zero_le _).trans_lt (lt_blsub f 0 ho)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r]
     (f : ∀ a < type r, Ordinal.{max u v}) :
     blsub.{_, v} (type r) f = lsub.{_, v} fun a => f (typein r a) (typein_lt_type _ _) :=
   eq_of_forall_ge_iff fun o => by
     rw [blsub_le_iff, lsub_le_iff]
     exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r ⟨i, h⟩)⟩
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_const {o : Ordinal} (ho : o ≠ 0) (a : Ordinal) :
     (blsub.{u, v} o fun _ _ => a) = succ a :=
   bsup_const.{u, v} ho (succ a)
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_one (f : ∀ a < (1 : Ordinal), Ordinal) : blsub 1 f = succ (f 0 zero_lt_one) :=
   bsup_one _
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_id : ∀ o, (blsub.{u, u} o fun x _ => x) = o :=
   lsub_typein
 
@@ -811,18 +850,24 @@ theorem bsup_id_add_one (o) : (bsup.{u, u} (o + 1) fun x _ => x) = o :=
 theorem bsup_id_succ (o) : (bsup.{u, u} (succ o) fun x _ => x) = o :=
   iSup_typein_succ
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_le_of_brange_subset {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal}
     (h : brange o f ⊆ brange o' g) : blsub.{u, max v w} o f ≤ blsub.{v, max u w} o' g :=
   bsup_le_of_brange_subset.{u, v, w} fun a ⟨b, hb, hb'⟩ => by
     obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩
     simp_rw [← hc'] at hb'
     exact ⟨c, hc, hb'⟩
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_eq_of_brange_eq {o o'} {f : ∀ a < o, Ordinal} {g : ∀ a < o', Ordinal}
     (h : { o | ∃ i hi, f i hi = o } = { o | ∃ i hi, g i hi = o }) :
     blsub.{u, max v w} o f = blsub.{v, max u w} o' g :=
   (blsub_le_of_brange_subset.{u, v, w} h.le).antisymm (blsub_le_of_brange_subset.{v, u, w} h.ge)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem bsup_comp {o o' : Ordinal.{max u v}} {f : ∀ a < o, Ordinal.{max u v w}}
     (hf : ∀ {i j} (hi) (hj), i ≤ j → f i hi ≤ f j hj) {g : ∀ a < o', Ordinal.{max u v}}
     (hg : blsub.{_, u} o' g = o) :
@@ -833,22 +878,29 @@ theorem bsup_comp {o o' : Ordinal.{max u v}} {f : ∀ a < o, Ordinal.{max u v w}
     rcases hi with ⟨j, hj, hj'⟩
     exact (hf _ _ hj').trans (le_bsup _ _ _)
 
+set_option linter.deprecated false in
+@[deprecated "blsub is deprecated" (since := "2026-03-23")]
 theorem blsub_comp {o o' : Ordinal.{max u v}} {f : ∀ a < o, Ordinal.{max u v w}}
     (hf : ∀ {i j} (hi) (hj), i ≤ j → f i hi ≤ f j hj) {g : ∀ a < o', Ordinal.{max u v}}
     (hg : blsub.{_, u} o' g = o) :
     (blsub.{_, w} o' fun a ha => f (g a ha) (by rw [← hg]; apply lt_blsub)) = blsub.{_, w} o f :=
   @bsup_comp.{u, v, w} o _ (fun a ha => succ (f a ha))
     (fun {_ _} _ _ h => succ_le_succ_iff.2 (hf _ _ h)) g hg
 
+@[deprecated IsNormal.apply_of_isSuccLimit (since := "2026-03-23")]
 theorem IsNormal.bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}}
     (h : IsSuccLimit o) : (Ordinal.bsup.{_, v} o fun x _ => f x) = f o := by
   rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.ne_bot, bsup_id_limit fun _ ↦ h.succ_lt]
 
+set_option linter.deprecated false in
+@[deprecated IsNormal.apply_of_isSuccLimit (since := "2026-03-23")]
 theorem IsNormal.blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}}
     (h : IsSuccLimit o) : (blsub.{_, v} o fun x _ => f x) = f o := by
   rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h]
   exact fun a _ => H.strictMono (lt_succ a)
 
+set_option linter.deprecated false in
+@[deprecated isNormal_iff (since := "2026-03-23")]
 theorem isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} :
     IsNormal f ↔ (∀ a, f a < f (succ a)) ∧
       ∀ o, IsSuccLimit o → (bsup.{_, v} o fun x _ => f x) = f o :=
@@ -857,6 +909,8 @@ theorem isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}}
       rw [← h₂ _ ho]
       simpa [IsLUB, upperBounds, lowerBounds, IsLeast, bsup_le_iff] using le_bsup _⟩
 
+set_option linter.deprecated false in
+@[deprecated isNormal_iff (since := "2026-03-23")]
 theorem isNormal_iff_lt_succ_and_blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} :
     IsNormal f ↔ (∀ a, f a < f (succ a)) ∧
       ∀ o, IsSuccLimit o → (blsub.{_, v} o fun x _ => f x) = f o := by

Mathlib/SetTheory/Ordinal/FundamentalSequence.lean

@@ -121,6 +121,7 @@ theorem exists_isFundamentalSeq (ha : o.cof.ord = a) : ∃ f : Iio a → Iio o,
 
 /-! ### Deprecated material -/
 
+set_option linter.deprecated false in
 /-- A fundamental sequence for `a` is an increasing sequence of length `o = cof a` that converges at
     `a`. We provide `o` explicitly in order to avoid type rewrites. -/
 @[deprecated IsFundamentalSeq (since := "2026-03-23")]