chore(Init): add deprecation dates; remove long-deprecated items (#12347

)

All removed items are virtually unused in mathlib and have been deprecated for over a year.

Mathlib/Init/Core.lean

@@ -129,10 +129,7 @@ def PProd.mk.injArrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂
 #align has_lt.lt LT.lt
 #align has_append Append
 
-@[deprecated AndThen]
-class AndThen' (α : Type u) (β : Type v) (σ : outParam <| Type w) where
-  andthen : α → β → σ
-#align has_andthen AndThen'
+#align has_andthen AndThen
 
 #align has_union Union
 #align has_equiv HasEquivₓ -- universe levels don't match
@@ -158,15 +155,6 @@ class AndThen' (α : Type u) (β : Type v) (σ : outParam <| Type w) where
 
 attribute [simp] insert_emptyc_eq
 
-@[deprecated] def Std.Priority.default : Nat := 1000
-@[deprecated] def Std.Priority.max : Nat := 4294967295
-set_option linter.deprecated false in
-@[deprecated] protected def Nat.prio := Std.Priority.default + 100
-@[deprecated] def Std.Prec.max : Nat := 1024
-@[deprecated] def Std.Prec.arrow : Nat := 25
-set_option linter.deprecated false in
-@[deprecated] def Std.Prec.maxPlus : Nat := Std.Prec.max + 10
-
 #align has_sizeof SizeOf
 #align has_sizeof.sizeof SizeOf.sizeOf
 #align sizeof SizeOf.sizeOf
@@ -182,12 +170,5 @@ def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
 
 end Combinator
 
-@[deprecated] inductive BinTree (α : Type u)
-  | Empty : BinTree α
-  | leaf (val : α) : BinTree α
-  | node (left right : BinTree α) : BinTree α
-
-attribute [elab_without_expected_type] BinTree.node BinTree.leaf
-
 #align function.const_apply Function.const_apply
 #align function.comp_apply Function.comp_apply

Mathlib/Init/Data/List/Basic.lean

@@ -26,12 +26,12 @@ open Option Nat
 #align list.nth List.get?
 
 /-- nth element of a list `l` given `n < l.length`. -/
-@[deprecated get]
+@[deprecated get] -- 2023-01-05
 def nthLe (l : List α) (n) (h : n < l.length) : α := get l ⟨n, h⟩
 #align list.nth_le List.nthLe
 
 set_option linter.deprecated false in
-@[deprecated]
+@[deprecated] -- 2023-01-05
 theorem nthLe_eq (l : List α) (n) (h : n < l.length) : nthLe l n h = get l ⟨n, h⟩ := rfl
 
 /-- The head of a list, or the default element of the type is the list is `nil`. -/
@@ -49,10 +49,7 @@ def headI [Inhabited α] : List α → α
 
 #align list.map_with_index List.mapIdx
 
-/-- Find index of element with given property. -/
-@[deprecated findIdx]
-def findIndex (p : α → Prop) [DecidablePred p] : List α → ℕ := List.findIdx p
-#align list.find_index List.findIndex
+#align list.find_index List.findIdx
 
 #align list.update_nth List.set
 

Mathlib/Init/Logic.lean

@@ -14,30 +14,10 @@ set_option autoImplicit true
 
 #align opt_param_eq optParam_eq
 
-/- Implication -/
-
-@[deprecated] def Implies (a b : Prop) := a → b
-
-/-- Implication `→` is transitive. If `P → Q` and `Q → R` then `P → R`. -/
--- FIXME This should have `@[trans]`, but the `trans` attribute PR'd in #253 rejects it.
--- Note that it is still rejected after #857.
-@[deprecated] theorem Implies.trans {p q r : Prop} (h₁ : p → q) (h₂ : q → r) :
-    p → r := fun hp ↦ h₂ (h₁ hp)
-
-/- Not -/
-
-@[deprecated] def NonContradictory (a : Prop) : Prop := ¬¬a
-
 #align non_contradictory_intro not_not_intro
 
 /- Eq -/
 
-@[deprecated] theorem trans_rel_left {α : Sort u} {a b c : α}
-    (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c := h₂ ▸ h₁
-
-@[deprecated] theorem trans_rel_right {α : Sort u} {a b c : α}
-    (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c := h₁ ▸ h₂
-
 theorem not_of_eq_false {p : Prop} (h : p = False) : ¬p := fun hp ↦ h ▸ hp
 
 theorem cast_proof_irrel (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl
@@ -120,12 +100,10 @@ alias ⟨not_of_not_not_not, _⟩ := not_not_not
 -- FIXME
 -- attribute [congr] not_congr
 
-@[deprecated and_comm] theorem and_comm' (a b) : a ∧ b ↔ b ∧ a := and_comm
 #align and.comm and_comm
-#align and_comm and_comm'
+#align and_comm and_comm
 
-@[deprecated and_assoc] theorem and_assoc' (a b) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := and_assoc
-#align and_assoc and_assoc'
+#align and_assoc and_assoc
 #align and.assoc and_assoc
 
 #align and.left_comm and_left_comm
@@ -158,13 +136,11 @@ theorem false_and_iff : False ∧ p ↔ False := iff_of_eq (false_and _)
 #align eq_true_intro eq_true
 #align eq_false_intro eq_false
 
-@[deprecated or_comm] theorem or_comm' (a b) : a ∨ b ↔ b ∨ a := or_comm
 #align or.comm or_comm
-#align or_comm or_comm'
+#align or_comm or_comm
 
-@[deprecated or_assoc] theorem or_assoc' (a b) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := or_assoc
 #align or.assoc or_assoc
-#align or_assoc or_assoc'
+#align or_assoc or_assoc
 
 #align or_left_comm or_left_comm
 #align or.left_comm or_left_comm
@@ -318,9 +294,6 @@ alias by_cases := byCases
 alias by_contradiction := byContradiction
 alias not_not_iff := not_not
 
-@[deprecated not_or] theorem not_or_iff_and_not (p q) [Decidable p] [Decidable q] :
-    ¬(p ∨ q) ↔ ¬p ∧ ¬q := not_or
-
 end Decidable
 
 #align decidable_of_decidable_of_iff decidable_of_decidable_of_iff
@@ -376,9 +349,6 @@ theorem rec_subsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h
   | isTrue h => h₃ h
   | isFalse h => h₄ h
 
-@[deprecated ite_self]
-theorem if_t_t (c : Prop) [Decidable c] {α : Sort u} (t : α) : ite c t t = t := ite_self _
-
 theorem imp_of_if_pos {c t e : Prop} [Decidable c] (h : ite c t e) (hc : c) : t :=
   (if_pos hc ▸ h :)
 #align implies_of_if_pos imp_of_if_pos

Mathlib/RingTheory/Int/Basic.lean

@@ -182,18 +182,16 @@ theorem gcd_ne_one_iff_gcd_mul_right_ne_one {a : ℤ} {m n : ℕ} :
   simp only [gcd_eq_one_iff_coprime, ← not_and_or, not_iff_not, IsCoprime.mul_right_iff]
 #align int.gcd_ne_one_iff_gcd_mul_right_ne_one Int.gcd_ne_one_iff_gcd_mul_right_ne_one
 
-set_option linter.deprecated false in -- trans_rel_left
 /-- If `gcd a (m * n) = 1`, then `gcd a m = 1`. -/
 theorem gcd_eq_one_of_gcd_mul_right_eq_one_left {a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) :
     a.gcd m = 1 :=
-  Nat.dvd_one.mp <| trans_rel_left _ (gcd_dvd_gcd_mul_right_right a m n) h
+  Nat.dvd_one.mp <| h ▸ (gcd_dvd_gcd_mul_right_right a m n)
 #align int.gcd_eq_one_of_gcd_mul_right_eq_one_left Int.gcd_eq_one_of_gcd_mul_right_eq_one_left
 
-set_option linter.deprecated false in -- trans_rel_left
 /-- If `gcd a (m * n) = 1`, then `gcd a n = 1`. -/
 theorem gcd_eq_one_of_gcd_mul_right_eq_one_right {a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) :
     a.gcd n = 1 :=
-  Nat.dvd_one.mp <| trans_rel_left _ (gcd_dvd_gcd_mul_left_right a n m) h
+  Nat.dvd_one.mp <| h ▸ (gcd_dvd_gcd_mul_left_right a n m)
 #align int.gcd_eq_one_of_gcd_mul_right_eq_one_right Int.gcd_eq_one_of_gcd_mul_right_eq_one_right
 
 theorem sq_of_gcd_eq_one {a b c : ℤ} (h : Int.gcd a b = 1) (heq : a * b = c ^ 2) :

scripts/nolints.json

@@ -1,8 +1,6 @@
-[["docBlame", "AndThen'"],
- ["docBlame", "AsFalse"],
+[["docBlame", "AsFalse"],
  ["docBlame", "AsTrue"],
  ["docBlame", "Associative"],
- ["docBlame", "BinTree"],
  ["docBlame", "Commutative"],
  ["docBlame", "Computable"],
  ["docBlame", "Computable₂"],
@@ -11,7 +9,6 @@
  ["docBlame", "Cont"],
  ["docBlame", "ContT"],
  ["docBlame", "ExistsUnique"],
- ["docBlame", "Implies"],
  ["docBlame", "IsDecEq"],
  ["docBlame", "IsDecRefl"],
  ["docBlame", "IsIdempotent"],
@@ -25,7 +22,6 @@
  ["docBlame", "LeftIdentity"],
  ["docBlame", "MonadCont"],
  ["docBlame", "MonadWriter"],
- ["docBlame", "NonContradictory"],
  ["docBlame", "One"],
  ["docBlame", "Partrec"],
  ["docBlame", "Partrec₂"],
@@ -85,7 +81,6 @@
  ["docBlame", "AlgHom.toAddMonoidHom'"],
  ["docBlame", "AlgHom.toMonoidHom'"],
  ["docBlame", "AlgebraCat.carrier"],
- ["docBlame", "AndThen'.andthen"],
  ["docBlame", "Bifunctor.bimap"],
  ["docBlame", "BilinForm.bilin"],
  ["docBlame", "Bimod.X"],
@@ -1019,5 +1014,4 @@
  ["docBlame", "Mathlib.Meta.NormNum.evalAdd.core.ratArm"],
  ["docBlame", "Mathlib.Meta.NormNum.evalMul.core.intArm"],
  ["docBlame", "Mathlib.Meta.NormNum.evalMul.core.ratArm"],
- ["unusedArguments", "Combinator.K"],
- ["unusedArguments", "Decidable.not_or_iff_and_not"]]
+ ["unusedArguments", "Combinator.K"]]

scripts/noshake.json

@@ -315,6 +315,7 @@
   "Mathlib.Lean.Expr.Basic": ["Std.Logic"],
   "Mathlib.Init.Data.Nat.Lemmas": ["Std.WF"],
   "Mathlib.Init.Data.Nat.GCD": ["Std.Data.Nat.Gcd"],
+  "Mathlib.Init.Data.List.Basic": ["Std.Data.List.Basic"],
   "Mathlib.Init.Data.Int.Basic": ["Std.Data.Int.Order"],
   "Mathlib.Init.Core": ["Std.Classes.Dvd"],
   "Mathlib.GroupTheory.Subgroup.Order": ["Mathlib.GroupTheory.Submonoid.Order"],