more

Author: kim-em

src/Std/Data/DTreeMap/Basic.lean

@@ -280,21 +280,13 @@ map is empty.
 def minEntry? (t : DTreeMap α β cmp) : Option ((a : α) × β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.minEntry?
 
-@[inline, inherit_doc minEntry?, deprecated minEntry? (since := "2025-03-13")]
-def min? (t : DTreeMap α β cmp) : Option ((a : α) × β a) :=
-  t.minEntry?
-
 /--
 Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.
 -/
 @[inline]
 def minEntry (t : DTreeMap α β cmp) (h : t.isEmpty = false) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.minEntry h
 
-@[inline, inherit_doc minEntry, deprecated minEntry (since := "2025-03-13")]
-def min (t : DTreeMap α β cmp) (h : t.isEmpty = false) : (a : α) × β a :=
-  t.minEntry h
-
 /--
 Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
 empty.
@@ -303,10 +295,6 @@ empty.
 def minEntry! [Inhabited ((a : α) × β a)] (t : DTreeMap α β cmp) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.minEntry!
 
-@[inline, inherit_doc minEntry!, deprecated minEntry! (since := "2025-03-13")]
-def min! [Inhabited ((a : α) × β a)] (t : DTreeMap α β cmp) : (a : α) × β a :=
-  t.minEntry!
-
 /--
 Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
 the tree map is empty.
@@ -315,10 +303,6 @@ the tree map is empty.
 def minEntryD (t : DTreeMap α β cmp) (fallback : (a : α) × β a) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.minEntryD fallback
 
-@[inline, inherit_doc minEntryD, deprecated minEntryD (since := "2025-03-13")]
-def minD (t : DTreeMap α β cmp) (fallback : (a : α) × β a) : (a : α) × β a :=
-  t.minEntryD fallback
-
 /--
 Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
 map is empty.
@@ -327,21 +311,13 @@ map is empty.
 def maxEntry? (t : DTreeMap α β cmp) : Option ((a : α) × β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.maxEntry?
 
-@[inline, inherit_doc maxEntry?, deprecated maxEntry? (since := "2025-03-13")]
-def max? (t : DTreeMap α β cmp) : Option ((a : α) × β a) :=
-  t.maxEntry?
-
 /--
 Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.
 -/
 @[inline]
 def maxEntry (t : DTreeMap α β cmp) (h : t.isEmpty = false) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.maxEntry h
 
-@[inline, inherit_doc maxEntry, deprecated maxEntry (since := "2025-03-13")]
-def max (t : DTreeMap α β cmp) (h : t.isEmpty = false) : (a : α) × β a :=
-  t.maxEntry h
-
 /--
 Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
 empty.
@@ -350,10 +326,6 @@ empty.
 def maxEntry! [Inhabited ((a : α) × β a)] (t : DTreeMap α β cmp) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.maxEntry!
 
-@[inline, inherit_doc maxEntry!, deprecated maxEntry! (since := "2025-03-13")]
-def max! [Inhabited ((a : α) × β a)] (t : DTreeMap α β cmp) : (a : α) × β a :=
-  t.maxEntry!
-
 /--
 Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
 the tree map is empty.
@@ -362,10 +334,6 @@ the tree map is empty.
 def maxEntryD (t : DTreeMap α β cmp) (fallback : (a : α) × β a) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.maxEntryD fallback
 
-@[inline, inherit_doc maxEntryD, deprecated maxEntryD (since := "2025-03-13")]
-def maxD (t : DTreeMap α β cmp) (fallback : (a : α) × β a) : (a : α) × β a :=
-  t.maxEntryD fallback
-
 /--
 Tries to retrieve the smallest key in the tree map, returning `none` if the map is empty.
 -/
@@ -448,37 +416,21 @@ def entryAtIdxD (t : DTreeMap α β cmp) (n : Nat)
 def keyAtIdx? (t : DTreeMap α β cmp) (n : Nat) : Option α :=
   letI : Ord α := ⟨cmp⟩; Impl.keyAtIdx? t.inner n
 
-@[inline, inherit_doc keyAtIdx?, deprecated keyAtIdx? (since := "2025-03-25")]
-def keyAtIndex? (t : DTreeMap α β cmp) (n : Nat) : Option α :=
-  keyAtIdx? t n
-
 /-- Returns the `n`-th smallest key. -/
 @[inline]
 def keyAtIdx (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : α :=
   letI : Ord α := ⟨cmp⟩; Impl.keyAtIdx t.inner t.wf.balanced n h
 
-@[inline, inherit_doc keyAtIdx, deprecated keyAtIdx (since := "2025-03-25")]
-def keyAtIndex (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : α :=
-  keyAtIdx t n h
-
 /-- Returns the `n`-th smallest key, or panics if `n` is at least `t.size`. -/
 @[inline]
 def keyAtIdx! [Inhabited α] (t : DTreeMap α β cmp) (n : Nat) : α :=
   letI : Ord α := ⟨cmp⟩; t.inner.keyAtIdx! n
 
-@[inline, inherit_doc keyAtIdx!, deprecated keyAtIdx! (since := "2025-03-25")]
-def keyAtIndex! [Inhabited α] (t : DTreeMap α β cmp) (n : Nat) : α :=
-  keyAtIdx! t n
-
 /-- Returns the `n`-th smallest key, or `fallback` if `n` is at least `t.size`. -/
 @[inline]
 def keyAtIdxD (t : DTreeMap α β cmp) (n : Nat) (fallback : α) : α :=
   letI : Ord α := ⟨cmp⟩; t.inner.keyAtIdxD n fallback
 
-@[inline, inherit_doc keyAtIdxD, deprecated keyAtIdxD (since := "2025-03-25")]
-def keyAtIndexD (t : DTreeMap α β cmp) (n : Nat) (fallback : α) : α :=
-  keyAtIdxD t n fallback
-
 /--
 Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
 given key, returning `none` if no such pair exists.
@@ -712,66 +664,34 @@ def getD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=
 def minEntry? (t : DTreeMap α β cmp) : Option (α × β) :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntry? t.inner
 
-@[inline, inherit_doc minEntry?, deprecated minEntry? (since := "2025-03-13")]
-def min? (t : DTreeMap α β cmp) : Option (α × β) :=
-  minEntry? t
-
 @[inline, inherit_doc DTreeMap.minEntry]
 def minEntry (t : DTreeMap α β cmp) (h : t.isEmpty = false) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntry t.inner h
 
-@[inline, inherit_doc minEntry, deprecated minEntry (since := "2025-03-13")]
-def min (t : DTreeMap α β cmp) (h : t.isEmpty = false) : α × β :=
-  minEntry t h
-
 @[inline, inherit_doc DTreeMap.minEntry!]
 def minEntry! [Inhabited (α × β)] (t : DTreeMap α β cmp) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntry! t.inner
 
-@[inline, inherit_doc minEntry!, deprecated minEntry! (since := "2025-03-13")]
-def min! [Inhabited (α × β)] (t : DTreeMap α β cmp) : α × β :=
-  minEntry! t
-
 @[inline, inherit_doc DTreeMap.minEntryD]
 def minEntryD (t : DTreeMap α β cmp) (fallback : α × β) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntryD t.inner fallback
 
-@[inline, inherit_doc minEntryD, deprecated minEntryD (since := "2025-03-13")]
-def minD (t : DTreeMap α β cmp) (fallback : α × β) : α × β :=
-  minEntryD t fallback
-
 @[inline, inherit_doc DTreeMap.maxEntry?]
 def maxEntry? (t : DTreeMap α β cmp) : Option (α × β) :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.maxEntry? t.inner
 
-@[inline, inherit_doc maxEntry?, deprecated maxEntry? (since := "2025-03-13")]
-def max? (t : DTreeMap α β cmp) : Option (α × β) :=
-  maxEntry? t
-
 @[inline, inherit_doc DTreeMap.maxEntry]
 def maxEntry (t : DTreeMap α β cmp) (h : t.isEmpty = false) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.maxEntry t.inner h
 
-@[inline, inherit_doc maxEntry, deprecated maxEntry (since := "2025-03-13")]
-def max (t : DTreeMap α β cmp) (h : t.isEmpty = false) : α × β :=
-  maxEntry t h
-
 @[inline, inherit_doc DTreeMap.maxEntry!]
 def maxEntry! [Inhabited (α × β)] (t : DTreeMap α β cmp) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.maxEntry! t.inner
 
-@[inline, inherit_doc maxEntry!, deprecated maxEntry! (since := "2025-03-13")]
-def max! [Inhabited (α × β)] (t : DTreeMap α β cmp) : α × β :=
-  maxEntry! t
-
 @[inline, inherit_doc DTreeMap.maxEntryD]
 def maxEntryD (t : DTreeMap α β cmp) (fallback : α × β) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.maxEntryD t.inner fallback
 
-@[inline, inherit_doc maxEntryD, deprecated maxEntryD (since := "2025-03-13")]
-def maxD (t : DTreeMap α β cmp) (fallback : α × β) : α × β :=
-  maxEntryD t fallback
-
 @[inline, inherit_doc DTreeMap.entryAtIdx?]
 def entryAtIdx? (t : DTreeMap α β cmp) (n : Nat) : Option (α × β) :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.entryAtIdx? t.inner n

src/Std/Data/DTreeMap/Lemmas.lean

@@ -1297,14 +1297,6 @@ theorem forMUncurried_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β →
     forMUncurried f t = (Const.toList t).forM f :=
   Impl.Const.forM_eq_forM_toList
 
-/--
-Deprecated, use `forMUncurried_eq_forM_toList` together with `forM_eq_forMUncurried` instead.
--/
-@[deprecated forMUncurried_eq_forM_toList (since := "2025-03-02")]
-theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α → β → m PUnit} :
-    t.forM f = (Const.toList t).forM (fun a => f a.1 a.2) :=
-  Impl.Const.forM_eq_forM_toList
-
 theorem forIn_eq_forInUncurried [Monad m] [LawfulMonad m]
     {f : α → β → δ → m (ForInStep δ)} {init : δ} :
     t.forIn f init = forInUncurried (fun a b => f a.1 a.2 b) init t := rfl
@@ -1314,15 +1306,6 @@ theorem forInUncurried_eq_forIn_toList [Monad m] [LawfulMonad m]
     forInUncurried f init t = ForIn.forIn (Const.toList t) init f :=
   Impl.Const.forIn_eq_forIn_toList
 
-/--
-Deprecated, use `forInUncurried_eq_forIn_toList` together with `forIn_eq_forInUncurried` instead.
--/
-@[deprecated forInUncurried_eq_forIn_toList (since := "2025-03-02")]
-theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
-    {f : α → β → δ → m (ForInStep δ)} {init : δ} :
-    t.forIn f init = ForIn.forIn (Const.toList t) init (fun a b => f a.1 a.2 b) :=
-  Impl.Const.forIn_eq_forIn_toList
-
 end Const
 
 end monadic

src/Std/Data/DTreeMap/Raw/Basic.lean

@@ -202,10 +202,6 @@ def getKeyD (t : Raw α β cmp) (a : α) (fallback : α) : α :=
 def minEntry? (t : Raw α β cmp) : Option ((a : α) × β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.minEntry?
 
-@[inline, inherit_doc minEntry?, deprecated minEntry? (since := "2025-03-13")]
-def min? (t : Raw α β cmp) : Option ((a : α) × β a) :=
-  t.minEntry?
-
 /-!
 We do not provide `minEntry` for the raw trees.
 -/
@@ -214,26 +210,14 @@ We do not provide `minEntry` for the raw trees.
 def minEntry! [Inhabited ((a : α) × β a)] (t : Raw α β cmp) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.minEntry!
 
-@[inline, inherit_doc minEntry!, deprecated minEntry! (since := "2025-03-13")]
-def min! [Inhabited ((a : α) × β a)] (t : Raw α β cmp) : (a : α) × β a :=
-  t.minEntry!
-
 @[inline, inherit_doc DTreeMap.minEntryD]
 def minEntryD (t : Raw α β cmp) (fallback : (a : α) × β a) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.minEntryD fallback
 
-@[inline, inherit_doc minEntryD, deprecated minEntryD (since := "2025-03-13")]
-def minD (t : Raw α β cmp) (fallback : (a : α) × β a) : (a : α) × β a :=
-  t.minEntryD fallback
-
 @[inline, inherit_doc DTreeMap.maxEntry?]
 def maxEntry? (t : Raw α β cmp) : Option ((a : α) × β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.maxEntry?
 
-@[inline, inherit_doc maxEntry?, deprecated maxEntry? (since := "2025-03-13")]
-def max? (t : Raw α β cmp) : Option ((a : α) × β a) :=
-  t.maxEntry?
-
 /-!
 We do not provide `maxEntry` for the raw trees.
 -/
@@ -242,18 +226,10 @@ We do not provide `maxEntry` for the raw trees.
 def maxEntry! [Inhabited ((a : α) × β a)] (t : Raw α β cmp) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.maxEntry!
 
-@[inline, inherit_doc maxEntry!, deprecated maxEntry! (since := "2025-03-13")]
-def max! [Inhabited ((a : α) × β a)] (t : Raw α β cmp) : (a : α) × β a :=
-  t.maxEntry!
-
 @[inline, inherit_doc DTreeMap.maxEntryD]
 def maxEntryD (t : Raw α β cmp) (fallback : (a : α) × β a) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.maxEntryD fallback
 
-@[inline, inherit_doc maxEntryD, deprecated maxEntryD (since := "2025-03-13")]
-def maxD (t : Raw α β cmp) (fallback : (a : α) × β a) : (a : α) × β a :=
-  t.maxEntryD fallback
-
 @[inline, inherit_doc DTreeMap.minKey?]
 def minKey? (t : Raw α β cmp) : Option α :=
   letI : Ord α := ⟨cmp⟩; t.inner.minKey?
@@ -306,10 +282,6 @@ def entryAtIdxD (t : Raw α β cmp) (n : Nat) (fallback : (a : α) × β a) : (a
 def keyAtIdx? (t : Raw α β cmp) (n : Nat) : Option α :=
   letI : Ord α := ⟨cmp⟩; Impl.keyAtIdx? t.inner n
 
-@[inline, inherit_doc DTreeMap.keyAtIdx?, deprecated keyAtIdx? (since := "2025-03-25")]
-def keyAtIndex? (t : Raw α β cmp) (n : Nat) : Option α :=
-  keyAtIdx? t n
-
 /-!
 We do not provide `keyAtIdx` for the raw trees.
 -/
@@ -318,18 +290,10 @@ We do not provide `keyAtIdx` for the raw trees.
 def keyAtIdx! [Inhabited α] (t : Raw α β cmp) (n : Nat) : α :=
   letI : Ord α := ⟨cmp⟩; t.inner.keyAtIdx! n
 
-@[inline, inherit_doc DTreeMap.keyAtIdx!, deprecated keyAtIdx! (since := "2025-03-25")]
-def keyAtIndex! [Inhabited α] (t : Raw α β cmp) (n : Nat) : α :=
-  keyAtIdx! t n
-
 @[inline, inherit_doc DTreeMap.keyAtIdxD]
 def keyAtIdxD (t : Raw α β cmp) (n : Nat) (fallback : α) : α :=
   letI : Ord α := ⟨cmp⟩; t.inner.keyAtIdxD n fallback
 
-@[inline, inherit_doc DTreeMap.keyAtIdxD, deprecated keyAtIdxD (since := "2025-03-25")]
-def keyAtIndexD (t : Raw α β cmp) (n : Nat) (fallback : α) : α :=
-  keyAtIdxD t n fallback
-
 @[inline, inherit_doc DTreeMap.getEntryGE?]
 def getEntryGE? (t : Raw α β cmp) (k : α) : Option ((a : α) × β a) :=
   letI : Ord α := ⟨cmp⟩; Impl.getEntryGE? k t.inner
@@ -464,10 +428,6 @@ def getD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
 def minEntry? (t : Raw α β cmp) : Option (α × β) :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntry? t.inner
 
-@[inline, inherit_doc minEntry?, deprecated minEntry? (since := "2025-03-13")]
-def min? (t : Raw α β cmp) : Option (α × β) :=
-  minEntry? t
-
 /-!
 We do not provide `minEntry` for the raw trees.
 -/
@@ -476,42 +436,22 @@ We do not provide `minEntry` for the raw trees.
 def minEntry! [Inhabited (α × β)] (t : Raw α β cmp) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntry! t.inner
 
-@[inline, inherit_doc minEntry!, deprecated minEntry! (since := "2025-03-13")]
-def min! [Inhabited (α × β)] (t : Raw α β cmp) : α × β :=
-  minEntry! t
-
 @[inline, inherit_doc DTreeMap.Const.minEntryD]
 def minEntryD (t : Raw α β cmp) (fallback : α × β) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntryD t.inner fallback
 
-@[inline, inherit_doc minEntryD, deprecated minEntryD (since := "2025-03-13")]
-def minD (t : Raw α β cmp) (fallback : α × β) : α × β :=
-  minEntryD t fallback
-
 @[inline, inherit_doc DTreeMap.Const.maxEntry?]
 def maxEntry? (t : Raw α β cmp) : Option (α × β) :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.maxEntry? t.inner
 
-@[inline, inherit_doc maxEntry?, deprecated maxEntry? (since := "2025-03-13")]
-def max? (t : Raw α β cmp) : Option (α × β) :=
-  maxEntry? t
-
 @[inline, inherit_doc DTreeMap.Const.maxEntry!]
 def maxEntry! [Inhabited (α × β)] (t : Raw α β cmp) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.maxEntry! t.inner
 
-@[inline, inherit_doc maxEntry!, deprecated maxEntry! (since := "2025-03-13")]
-def max! [Inhabited (α × β)] (t : Raw α β cmp) : α × β :=
-  maxEntry! t
-
 @[inline, inherit_doc DTreeMap.Const.maxEntryD]
 def maxEntryD (t : Raw α β cmp) (fallback : α × β) : α × β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.maxEntryD t.inner fallback
 
-@[inline, inherit_doc maxEntryD, deprecated maxEntryD (since := "2025-03-13")]
-def maxD (t : Raw α β cmp) (fallback : α × β) : α × β :=
-  maxEntryD t fallback
-
 @[inline, inherit_doc DTreeMap.Const.entryAtIdx?]
 def entryAtIdx? (t : Raw α β cmp) (n : Nat) : Option (α × β) :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.entryAtIdx? t.inner n

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -1305,32 +1305,6 @@ theorem forMUncurried_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β →
     forMUncurried f t = (Const.toList t).forM f :=
   Impl.Const.forM_eq_forM_toList
 
-/--
-Deprecated, use `forMUncurried_eq_forM_toList` together with `forM_eq_forMUncurried` instead.
--/
-@[deprecated forMUncurried_eq_forM_toList (since := "2025-03-02")]
-theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α → β → m PUnit} :
-    t.forM f = (Const.toList t).forM (fun a => f a.1 a.2) :=
-  Impl.Const.forM_eq_forM_toList
-
-theorem forIn_eq_forInUncurried [Monad m] [LawfulMonad m]
-    {f : α → β → δ → m (ForInStep δ)} {init : δ} :
-    t.forIn f init = forInUncurried (fun a b => f a.1 a.2 b) init t := rfl
-
-theorem forInUncurried_eq_forIn_toList [Monad m] [LawfulMonad m]
-    {f : α × β → δ → m (ForInStep δ)} {init : δ} :
-    forInUncurried f init t = ForIn.forIn (Const.toList t) init f :=
-  Impl.Const.forIn_eq_forIn_toList
-
-/--
-Deprecated, use `forInUncurried_eq_forIn_toList` together with `forIn_eq_forInUncurried` instead.
--/
-@[deprecated forInUncurried_eq_forIn_toList (since := "2025-03-02")]
-theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
-    {f : α → β → δ → m (ForInStep δ)} {init : δ} :
-    t.forIn f init = ForIn.forIn (Const.toList t) init (fun a b => f a.1 a.2 b) :=
-  Impl.Const.forIn_eq_forIn_toList
-
 end Const
 
 end monadic