diff --git a/Archive/Arithcc.lean b/Archive/Arithcc.lean
index 142a3ff54cfd5..0ce0533334b10 100644
--- a/Archive/Arithcc.lean
+++ b/Archive/Arithcc.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xi Wang
 -/
 import Mathlib.Order.Basic
-import Mathlib.Tactic.Basic
+import Mathlib.Data.Nat.Basic
+import Mathlib.Tactic.Common
 
 #align_import arithcc from "leanprover-community/mathlib"@"eb3595ed8610db8107b75b75ab64ab6390684155"
 
diff --git a/Mathlib.lean b/Mathlib.lean
index 55e0b30c0366f..4bb542f9d500b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2085,8 +2085,6 @@ import Mathlib.GroupTheory.Torsion
 import Mathlib.GroupTheory.Transfer
 import Mathlib.InformationTheory.Hamming
 import Mathlib.Init.Algebra.Classes
-import Mathlib.Init.Algebra.Functions
-import Mathlib.Init.Algebra.Order
 import Mathlib.Init.Align
 import Mathlib.Init.CCLemmas
 import Mathlib.Init.Classes.Order
@@ -2128,6 +2126,8 @@ import Mathlib.Init.Function
 import Mathlib.Init.IteSimp
 import Mathlib.Init.Logic
 import Mathlib.Init.Meta.WellFoundedTactics
+import Mathlib.Init.Order.Defs
+import Mathlib.Init.Order.LinearOrder
 import Mathlib.Init.Propext
 import Mathlib.Init.Quot
 import Mathlib.Init.Set
diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean
index cdfabedf944a9..d44fbea65607f 100644
--- a/Mathlib/Algebra/CharZero/Defs.lean
+++ b/Mathlib/Algebra/CharZero/Defs.lean
@@ -3,6 +3,7 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Tactic.NormCast.Tactic
 import Mathlib.Algebra.NeZero
diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean
index 907abb6ac2229..f02a9ba57b66c 100644
--- a/Mathlib/Algebra/Field/Defs.lean
+++ b/Mathlib/Algebra/Field/Defs.lean
@@ -179,3 +179,8 @@ end Field
 `NeZero` should not be needed in the basic algebraic hierarchy.
 -/
 assert_not_exists NeZero
+
+/-
+Check that we have not imported `Mathlib.Tactic.Common` yet.
+-/
+assert_not_exists Mathlib.Tactic.LibrarySearch.librarySearch
diff --git a/Mathlib/Algebra/Field/IsField.lean b/Mathlib/Algebra/Field/IsField.lean
index 6f42b1f682fc8..e75c8f9db21c4 100644
--- a/Mathlib/Algebra/Field/IsField.lean
+++ b/Mathlib/Algebra/Field/IsField.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Field.Defs
+import Mathlib.Tactic.Common
 
 #align_import algebra.field.defs from "leanprover-community/mathlib"@"2651125b48fc5c170ab1111afd0817c903b1fc6c"
 
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index 3d19fa4e9795a..25204fff3b1b0 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Tactic.Common
 
 #align_import algebra.group.basic from "leanprover-community/mathlib"@"a07d750983b94c530ab69a726862c2ab6802b38c"
 
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index e8d6835dd9479..8b3c1b6cd6dfb 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -5,7 +5,8 @@ Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
 import Mathlib.Init.ZeroOne
 import Mathlib.Init.Data.Int.Basic
-import Mathlib.Tactic.Common
+import Mathlib.Logic.Function.Basic
+import Mathlib.Tactic.Basic
 
 #align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 
diff --git a/Mathlib/Algebra/NeZero.lean b/Mathlib/Algebra/NeZero.lean
index b842eaacd7883..00b8c17c45bd4 100644
--- a/Mathlib/Algebra/NeZero.lean
+++ b/Mathlib/Algebra/NeZero.lean
@@ -5,7 +5,7 @@ Authors: Eric Rodriguez
 -/
 import Mathlib.Logic.Basic
 import Mathlib.Init.ZeroOne
-import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Order.Defs
 
 #align_import algebra.ne_zero from "leanprover-community/mathlib"@"f340f229b1f461aa1c8ee11e0a172d0a3b301a4a"
 
diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean
index 393b9e38a9538..87f580c7a24c8 100644
--- a/Mathlib/Algebra/Ring/Defs.lean
+++ b/Mathlib/Algebra/Ring/Defs.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Ne
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Data.Int.Cast.Defs
+import Mathlib.Tactic.Spread
 import Mathlib.Util.AssertExists
 
 #align_import algebra.ring.defs from "leanprover-community/mathlib"@"76de8ae01554c3b37d66544866659ff174e66e1f"
diff --git a/Mathlib/Control/Random.lean b/Mathlib/Control/Random.lean
index f409d1ccfb95d..86a8005839d48 100644
--- a/Mathlib/Control/Random.lean
+++ b/Mathlib/Control/Random.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 
-import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Order.Defs
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Init.Data.Int.Order
 import Mathlib.Control.ULiftable
diff --git a/Mathlib/Data/Char.lean b/Mathlib/Data/Char.lean
index 93f5545cfeb2e..f65f640dbb6ed 100644
--- a/Mathlib/Data/Char.lean
+++ b/Mathlib/Data/Char.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.UInt
-import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Order.Defs
 
 #align_import data.char from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 
diff --git a/Mathlib/Data/FunLike/Basic.lean b/Mathlib/Data/FunLike/Basic.lean
index 438496da1ff8f..03adb43051e4f 100644
--- a/Mathlib/Data/FunLike/Basic.lean
+++ b/Mathlib/Data/FunLike/Basic.lean
@@ -5,6 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.Logic.Function.Basic
 import Mathlib.Tactic.NormCast
+import Mathlib.Util.CompileInductive
 
 #align_import data.fun_like.basic from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
diff --git a/Mathlib/Data/Int/Cast/Basic.lean b/Mathlib/Data/Int/Cast/Basic.lean
index 1a434670cdc7e..f003f4cbd1703 100644
--- a/Mathlib/Data/Int/Cast/Basic.lean
+++ b/Mathlib/Data/Int/Cast/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
+import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Algebra.Group.Basic
 
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
index 9251d428ce9e3..3341df765f725 100644
--- a/Mathlib/Data/Nat/Basic.lean
+++ b/Mathlib/Data/Nat/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights r
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
+import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Order.Basic
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.Ring.Defs
diff --git a/Mathlib/Data/Nat/Cast/Defs.lean b/Mathlib/Data/Nat/Cast/Defs.lean
index 580984e5c486e..be1783b58c5d9 100644
--- a/Mathlib/Data/Nat/Cast/Defs.lean
+++ b/Mathlib/Data/Nat/Cast/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Tactic.SplitIfs
 
 #align_import data.nat.cast.defs from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean
index 2b2e0fd416032..f770c1475e3fd 100644
--- a/Mathlib/Data/Option/Basic.lean
+++ b/Mathlib/Data/Option/Basic.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Option.Defs
 import Mathlib.Logic.IsEmpty
 import Mathlib.Logic.Relator
 import Mathlib.Tactic.Common
+import Mathlib.Util.CompileInductive
 
 #align_import data.option.basic from "leanprover-community/mathlib"@"f340f229b1f461aa1c8ee11e0a172d0a3b301a4a"
 
diff --git a/Mathlib/Data/PNat/Defs.lean b/Mathlib/Data/PNat/Defs.lean
index 9cb964fd26e11..ab5e760ccfd6d 100644
--- a/Mathlib/Data/PNat/Defs.lean
+++ b/Mathlib/Data/PNat/Defs.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Neil Strickland
 -/
-
+import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Algebra.NeZero
 import Mathlib.Data.Nat.Cast.Defs
 import Mathlib.Order.Basic
diff --git a/Mathlib/Init/Data/Int/Order.lean b/Mathlib/Init/Data/Int/Order.lean
index 2b5e39db26d3b..ee3ee97195104 100644
--- a/Mathlib/Init/Data/Int/Order.lean
+++ b/Mathlib/Init/Data/Int/Order.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 
-import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Order.Defs
 import Mathlib.Init.Data.Int.Basic
 
 /-! # The order relation on the integers -/
diff --git a/Mathlib/Init/Data/Nat/Lemmas.lean b/Mathlib/Init/Data/Nat/Lemmas.lean
index b91f950c66540..9508ebb1078ad 100644
--- a/Mathlib/Init/Data/Nat/Lemmas.lean
+++ b/Mathlib/Init/Data/Nat/Lemmas.lean
@@ -6,7 +6,8 @@ Authors: Leonardo de Moura, Jeremy Avigad
 import Std.Data.Nat.Lemmas
 import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Init.Data.Nat.Div
-import Mathlib.Init.Algebra.Functions
+import Mathlib.Init.Order.LinearOrder
+import Mathlib.Tactic.Cases
 
 #align_import init.data.nat.lemmas from "leanprover-community/lean"@"38b59111b2b4e6c572582b27e8937e92fc70ac02"
 
@@ -673,16 +674,6 @@ instance decidableDvd : @DecidableRel ℕ (· ∣ ·) := fun _m _n =>
 
 #align nat.dvd_of_mul_dvd_mul_right Nat.dvd_of_mul_dvd_mul_rightₓ
 
-/-! iterate -/
-
-
-def iterate {α : Sort u} (op : α → α) : ℕ → α → α
-  | 0, a => a
-  | succ k, a => iterate op k (op a)
-#align nat.iterate Nat.iterate
-
-notation:max f "^["n"]" => iterate f n
-
 /-! find -/
 
 
diff --git a/Mathlib/Init/Algebra/Order.lean b/Mathlib/Init/Order/Defs.lean
similarity index 100%
rename from Mathlib/Init/Algebra/Order.lean
rename to Mathlib/Init/Order/Defs.lean
diff --git a/Mathlib/Init/Algebra/Functions.lean b/Mathlib/Init/Order/LinearOrder.lean
similarity index 96%
rename from Mathlib/Init/Algebra/Functions.lean
rename to Mathlib/Init/Order/LinearOrder.lean
index 7ed423578f7b6..56a5da05f8427 100644
--- a/Mathlib/Init/Algebra/Functions.lean
+++ b/Mathlib/Init/Order/LinearOrder.lean
@@ -3,10 +3,17 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
-import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Order.Defs
 
 #align_import init.algebra.functions from "leanprover-community/lean"@"c2bcdbcbe741ed37c361a30d38e179182b989f76"
 
+/-!
+# Basic lemmas about linear orders.
+
+The contents of this file came from `init.algebra.functions` in Lean 3,
+and it would be good to find everything a better home.
+-/
+
 universe u
 
 section
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 20e7575024a71..99aeced003ffb 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Logic.Nonempty
-import Mathlib.Init.Data.Nat.Lemmas
+import Mathlib.Tactic.Cases
 import Mathlib.Init.Set
 
 #align_import logic.function.basic from "leanprover-community/mathlib"@"29cb56a7b35f72758b05a30490e1f10bd62c35c1"
@@ -879,10 +879,6 @@ def Involutive {α} (f : α → α) : Prop :=
   ∀ x, f (f x) = x
 #align function.involutive Function.Involutive
 
-theorem involutive_iff_iter_2_eq_id {α} {f : α → α} : Involutive f ↔ f^[2] = id :=
-  funext_iff.symm
-#align function.involutive_iff_iter_2_eq_id Function.involutive_iff_iter_2_eq_id
-
 theorem _root_.Bool.involutive_not : Involutive not :=
   Bool.not_not
 
diff --git a/Mathlib/Logic/Function/Iterate.lean b/Mathlib/Logic/Function/Iterate.lean
index 85d5a8213f0a1..b01b35ddae986 100644
--- a/Mathlib/Logic/Function/Iterate.lean
+++ b/Mathlib/Logic/Function/Iterate.lean
@@ -34,6 +34,15 @@ universe u v
 
 variable {α : Type u} {β : Type v}
 
+/-- Iterate a function. -/
+def Nat.iterate {α : Sort u} (op : α → α) : ℕ → α → α
+  | 0, a => a
+  | succ k, a => iterate op k (op a)
+#align nat.iterate Nat.iterate
+
+@[inherit_doc Nat.iterate]
+notation:max f "^["n"]" => Nat.iterate f n
+
 namespace Function
 
 open Function (Commute)
@@ -231,11 +240,15 @@ alias ⟨iterate_cancel_of_add, _⟩ := iterate_add_eq_iterate
 #align function.iterate_cancel_of_add Function.iterate_cancel_of_add
 
 lemma iterate_cancel (hf : Injective f) (ha : f^[m] a = f^[n] a) : f^[m - n] a = a := by
-  obtain h | h := le_total m n
+  obtain h | h := Nat.le_total m n
   { simp [Nat.sub_eq_zero_of_le h] }
   { exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h]) }
 #align function.iterate_cancel Function.iterate_cancel
 
+theorem involutive_iff_iter_2_eq_id {α} {f : α → α} : Involutive f ↔ f^[2] = id :=
+  funext_iff.symm
+#align function.involutive_iff_iter_2_eq_id Function.involutive_iff_iter_2_eq_id
+
 end Function
 
 namespace List
diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index 1f36ff88bc019..d5774f116c31a 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro
 -/
+import Mathlib.Init.Order.LinearOrder
 import Mathlib.Data.Prod.Basic
 import Mathlib.Data.Subtype
 
diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean
index 2af31c5703cc9..2698fb1d3e50f 100644
--- a/Mathlib/Order/Lattice.lean
+++ b/Mathlib/Order/Lattice.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Data.Bool.Basic
-import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Order.Defs
 import Mathlib.Order.Monotone.Basic
 import Mathlib.Order.ULift
 import Mathlib.Tactic.GCongr.Core
diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean
index d46fd57540273..74d4f5fd77d63 100644
--- a/Mathlib/Order/Monotone/Basic.lean
+++ b/Mathlib/Order/Monotone/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro, Yaël Dillies
 -/
+import Mathlib.Logic.Function.Iterate
 import Mathlib.Init.Data.Int.Order
 import Mathlib.Order.Compare
 import Mathlib.Order.Max
diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean
index fc8358bb33e92..e9190a85885af 100644
--- a/Mathlib/Order/RelClasses.lean
+++ b/Mathlib/Order/RelClasses.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro, Yury G. Kudryashov
 -/
+import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Logic.IsEmpty
 import Mathlib.Logic.Relation
 import Mathlib.Order.Basic
diff --git a/Mathlib/Tactic/Basic.lean b/Mathlib/Tactic/Basic.lean
index e72f2743d0d1f..88a99c29d02eb 100644
--- a/Mathlib/Tactic/Basic.lean
+++ b/Mathlib/Tactic/Basic.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Kyle Miller
 -/
 import Lean
 import Std
-import Mathlib.Tactic.Cases
 
 set_option autoImplicit true
 
diff --git a/Mathlib/Tactic/GCongr/Core.lean b/Mathlib/Tactic/GCongr/Core.lean
index b4b9f4cab6649..4313b526578e6 100644
--- a/Mathlib/Tactic/GCongr/Core.lean
+++ b/Mathlib/Tactic/GCongr/Core.lean
@@ -3,7 +3,9 @@ Copyright (c) 2023 Mario Carneiro, Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Heather Macbeth
 -/
+import Mathlib.Init.Order.Defs
 import Mathlib.Tactic.Backtracking
+import Mathlib.Tactic.Core
 import Mathlib.Tactic.GCongr.ForwardAttr
 
 /-!
diff --git a/Mathlib/Tactic/PushNeg.lean b/Mathlib/Tactic/PushNeg.lean
index 78db3455cbb78..af5e1e6b273eb 100644
--- a/Mathlib/Tactic/PushNeg.lean
+++ b/Mathlib/Tactic/PushNeg.lean
@@ -7,7 +7,7 @@ Authors: Patrick Massot, Simon Hudon, Alice Laroche, Frédéric Dupuis, Jireh Lo
 import Lean
 import Mathlib.Lean.Expr
 import Mathlib.Logic.Basic
-import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Order.Defs
 import Mathlib.Tactic.Conv
 
 set_option autoImplicit true
diff --git a/test/Tauto.lean b/test/Tauto.lean
index 86937e5aa6ca8..4aa81764801e2 100644
--- a/test/Tauto.lean
+++ b/test/Tauto.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, David Renshaw
 -/
 import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.SplitIfs
 
 set_option autoImplicit true
 section tauto₀
diff --git a/test/push_neg.lean b/test/push_neg.lean
index 36e27e527537a..19a704266b3e6 100644
--- a/test/push_neg.lean
+++ b/test/push_neg.lean
@@ -5,7 +5,7 @@ Author: Alice Laroche, Frédéric Dupuis, Jireh Loreaux
 -/
 
 import Mathlib.Tactic.PushNeg
-import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Order.Defs
 
 set_option autoImplicit true
 variable {α β : Type} [LinearOrder β] {p q : Prop} {p' q' : α → Prop}