chore: move Init.Logic and its remaining dependencies to Deprecated (#17771)

The results in this file have been deprecated for a while and none seem to be used in Mathlib except for other deprecated results that aren't used either. So let's move everything to the `Deprecated` folder in order to empty out the `Init` folder.

Author: Vierkantor

Mathlib.lean

@@ -2657,6 +2657,8 @@ import Mathlib.Deprecated.Combinator
 import Mathlib.Deprecated.Equiv
 import Mathlib.Deprecated.Group
 import Mathlib.Deprecated.HashMap
+import Mathlib.Deprecated.Logic
+import Mathlib.Deprecated.MinMax
 import Mathlib.Deprecated.NatLemmas
 import Mathlib.Deprecated.RelClasses
 import Mathlib.Deprecated.Ring
@@ -2927,7 +2929,6 @@ import Mathlib.GroupTheory.Torsion
 import Mathlib.GroupTheory.Transfer
 import Mathlib.InformationTheory.Hamming
 import Mathlib.Init
-import Mathlib.Init.Logic
 import Mathlib.Lean.CoreM
 import Mathlib.Lean.Elab.Tactic.Basic
 import Mathlib.Lean.Elab.Term

Mathlib/Init/Logic.lean renamed to Mathlib/Deprecated/Logic.lean

@@ -6,12 +6,10 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 import Batteries.Tactic.Alias
 
 /-!
-# Note about `Mathlib/Init/`
-The files in `Mathlib/Init` are leftovers from the port from Mathlib3.
-(They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)
+# Note about deprecated files
 
-We intend to move all the content of these files out into the main `Mathlib` directory structure.
-Contributions assisting with this are appreciated.
+This file is deprecated, and is no longer imported by anything in mathlib other than other
+deprecated files, and test files. You should not need to import it.
 -/
 
 set_option linter.deprecated false

Mathlib/Deprecated/MinMax.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Mathlib.Deprecated.Logic
+import Mathlib.Order.MinMax
+/-!
+# Note about deprecated files
+
+This file is deprecated, and is no longer imported by anything in mathlib other than other
+deprecated files, and test files. You should not need to import it.
+-/
+
+universe u
+
+variable {α : Type u} [LinearOrder α]
+
+set_option linter.deprecated false
+
+@[deprecated instCommutativeMax (since := "2024-09-12")]
+theorem max_commutative : Commutative (α := α) max := max_comm
+@[deprecated instAssociativeMax (since := "2024-09-12")]
+theorem max_associative : Associative (α := α) max := max_assoc
+@[deprecated instCommutativeMin (since := "2024-09-12")]
+theorem min_commutative : Commutative (α := α) min := min_comm
+@[deprecated instAssociativeMin (since := "2024-09-12")]
+theorem min_associative : Associative (α := α) min := min_assoc

Mathlib/Order/MinMax.lean

@@ -3,7 +3,6 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Init.Logic
 import Mathlib.Logic.OpClass
 import Mathlib.Order.Lattice
 
@@ -244,18 +243,4 @@ instance instAssociativeMin : Std.Associative (α := α) min where assoc := min_
 theorem max_left_commutative : LeftCommutative (max : α → α → α) := ⟨max_left_comm⟩
 theorem min_left_commutative : LeftCommutative (min : α → α → α) := ⟨min_left_comm⟩
 
-section deprecated
-set_option linter.deprecated false
-
-@[deprecated instCommutativeMax (since := "2024-09-12")]
-theorem max_commutative : Commutative (α := α) max := max_comm
-@[deprecated instAssociativeMax (since := "2024-09-12")]
-theorem max_associative : Associative (α := α) max := max_assoc
-@[deprecated instCommutativeMin (since := "2024-09-12")]
-theorem min_commutative : Commutative (α := α) min := min_comm
-@[deprecated instAssociativeMin (since := "2024-09-12")]
-theorem min_associative : Associative (α := α) min := min_assoc
-
-end deprecated
-
 end

scripts/noshake.json

@@ -351,6 +351,7 @@
   "Mathlib.Geometry.Manifold.PoincareConjecture":
   ["Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected",
    "Mathlib.Util.Superscript"],
+  "Mathlib.Deprecated.MinMax": ["Mathlib.Order.MinMax"],
   "Mathlib.Data.Vector.Basic": ["Mathlib.Control.Applicative"],
   "Mathlib.Data.Set.Image": ["Batteries.Tactic.Congr"],
   "Mathlib.Data.Seq.Parallel": ["Mathlib.Init.Data.Prod"],