chore: remove >6 month deprecations (#5199)

src/Init/Data/BitVec/Lemmas.lean

@@ -152,9 +152,6 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
   getLsb (BitVec.ofNat n x) i = (i < n && x.testBit i) := by
   simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
 
-@[simp, deprecated toNat_ofNat (since := "2024-02-22")]
-theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
-
 @[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
 
 @[simp] theorem getMsb_zero : (0#w).getMsb i = false := by simp [getMsb]

src/Init/Data/Bool.lean

@@ -381,9 +381,6 @@ def toNat (b : Bool) : Nat := cond b 1 0
 theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
-@[deprecated toNat_le (since := "2024-02-23")]
-abbrev toNat_le_one := toNat_le
-
 theorem toNat_lt (b : Bool) : b.toNat < 2 :=
   Nat.lt_succ_of_le (toNat_le _)
 

src/Init/Data/Fin/Lemmas.lean

@@ -54,9 +54,6 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
   (Fin.ofNat' a is_pos).val = a % n := rfl
 
-@[deprecated ofNat'_zero_val (since := "2024-02-22")]
-theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
-
 @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
   rfl
 

src/Init/Data/Nat/Lemmas.lean

@@ -157,17 +157,9 @@ protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c
 protected theorem le_sub_iff_add_le {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ n + k ≤ m :=
   ⟨Nat.add_le_of_le_sub h, Nat.le_sub_of_add_le⟩
 
-@[deprecated Nat.le_sub_iff_add_le (since := "2024-02-19")]
-protected theorem add_le_to_le_sub (n : Nat) (h : m ≤ k) : n + m ≤ k ↔ n ≤ k - m :=
-  (Nat.le_sub_iff_add_le h).symm
-
 protected theorem add_le_of_le_sub' {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_comm .. ▸ Nat.add_le_of_le_sub h
 
-@[deprecated Nat.add_le_of_le_sub' (since := "2024-02-19")]
-protected theorem add_le_of_le_sub_left {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
-  Nat.add_le_of_le_sub' h
-
 protected theorem le_sub_of_add_le' {n k m : Nat} : m + n ≤ k → n ≤ k - m :=
   Nat.add_comm .. ▸ Nat.le_sub_of_add_le
 
@@ -429,14 +421,6 @@ protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min
 
 /-! ### mul -/
 
-@[deprecated Nat.mul_le_mul_left (since := "2024-02-19")]
-protected theorem mul_le_mul_of_nonneg_left {a b c : Nat} : a ≤ b → c * a ≤ c * b :=
-  Nat.mul_le_mul_left c
-
-@[deprecated Nat.mul_le_mul_right (since := "2024-02-19")]
-protected theorem mul_le_mul_of_nonneg_right {a b c : Nat} : a ≤ b → a * c ≤ b * c :=
-  Nat.mul_le_mul_right c
-
 protected theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m := by
   rw [Nat.mul_assoc, Nat.mul_comm m, ← Nat.mul_assoc]
 

src/Lean/Meta/Tactic/Replace.lean

@@ -190,10 +190,6 @@ def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (type
     | _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target"
   return mvarId
 
-@[deprecated MVarId.changeLocalDecl (since := "2022-07-15")]
-def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do
-  mvarId.changeLocalDecl fvarId typeNew checkDefEq
-
 /--
 Modify `mvarId` target type using `f`.
 -/

src/Lean/Widget/UserWidget.lean

@@ -357,15 +357,6 @@ structure UserWidgetDefinition where
 instance : ToModule UserWidgetDefinition where
   toModule uwd := { uwd with }
 
-@[deprecated (since := "2023-12-21")] private def widgetAttrImpl : AttributeImpl where
-  name := `widget
-  descr := "The `@[widget]` attribute has been deprecated, use `@[widget_module]` instead."
-  applicationTime := AttributeApplicationTime.afterCompilation
-  add := widgetModuleAttrImpl.add
-
-set_option linter.deprecated false in
-builtin_initialize registerBuiltinAttribute widgetAttrImpl
-
 private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
     (id : Name) : m UserWidgetDefinition := do
   ofExcept <| (← getEnv).evalConstCheck UserWidgetDefinition (← getOptions) ``UserWidgetDefinition id
@@ -374,13 +365,6 @@ private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadO
 opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
     (id : Name) : m UserWidgetDefinition
 
-/-- Save a user-widget instance to the infotree.
-    The given `widgetId` should be the declaration name of the widget definition. -/
-@[deprecated savePanelWidgetInfo (since := "2023-12-21")] def saveWidgetInfo (widgetId : Name) (props : Json)
-    (stx : Syntax) : CoreM Unit := do
-  let uwd ← evalUserWidgetDefinition widgetId
-  savePanelWidgetInfo (ToModule.toModule uwd).javascriptHash (pure props) stx
-
 /-! ## Retrieving panel widget instances -/
 
 /-- Retrieve all the `UserWidgetInfo`s that intersect a given line. -/
@@ -447,6 +431,4 @@ def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResp
 builtin_initialize
   Server.registerBuiltinRpcProcedure ``getWidgets _ _ getWidgets
 
-attribute [deprecated Module (since := "2023-12-21")] UserWidgetDefinition
-
 end Lean.Widget