diff --git a/Archive/Imo/Imo2008Q3.lean b/Archive/Imo/Imo2008Q3.lean
index 5b0da19bfbb31..badb86feb2481 100644
--- a/Archive/Imo/Imo2008Q3.lean
+++ b/Archive/Imo/Imo2008Q3.lean
@@ -82,6 +82,6 @@ theorem imo2008_q3 : ∀ N : ℕ, ∃ n : ℕ, n ≥ N ∧
   obtain ⟨n, hnat, hreal⟩ := p_lemma p hpp hpmod4 (by linarith [hineq₁, Nat.zero_le (N ^ 2)])
   have hineq₂ : n ^ 2 + 1 ≥ p := Nat.le_of_dvd (n ^ 2).succ_pos hnat
   have hineq₃ : n * n ≥ N * N := by linarith [hineq₁, hineq₂]
-  have hn_ge_N : n ≥ N := Nat.mul_self_le_mul_self_iff.mpr hineq₃
+  have hn_ge_N : n ≥ N := Nat.mul_self_le_mul_self_iff.1 hineq₃
   exact ⟨n, hn_ge_N, p, hpp, hnat, hreal⟩
 #align imo2008_q3 imo2008_q3
diff --git a/Archive/MiuLanguage/DecisionSuf.lean b/Archive/MiuLanguage/DecisionSuf.lean
index 218922a1de013..ad84b804cd278 100644
--- a/Archive/MiuLanguage/DecisionSuf.lean
+++ b/Archive/MiuLanguage/DecisionSuf.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gihan Marasingha
 -/
 import Archive.MiuLanguage.DecisionNec
-import Mathlib.Data.Nat.Pow
 import Mathlib.Tactic.Linarith
 
 #align_import miu_language.decision_suf from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"
diff --git a/Mathlib.lean b/Mathlib.lean
index 190c88a1decc9..be7a6473a7a39 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1942,7 +1942,6 @@ import Mathlib.Data.Nat.Pairing
 import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Nat.PartENat
 import Mathlib.Data.Nat.Periodic
-import Mathlib.Data.Nat.Pow
 import Mathlib.Data.Nat.Prime
 import Mathlib.Data.Nat.PrimeFin
 import Mathlib.Data.Nat.PrimeNormNum
diff --git a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
index dff6c91802c63..fdbc390a04a77 100644
--- a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
@@ -3,7 +3,10 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Data.List.BigOperators.Basic
+import Mathlib.Algebra.GroupPower.Hom
+import Mathlib.Algebra.GroupWithZero.Divisibility
+import Mathlib.Algebra.Order.Monoid.OrderDual
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Data.Multiset.Basic
 
 #align_import algebra.big_operators.multiset.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"
diff --git a/Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean b/Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
index e70c0d6f19991..0f37a957af95c 100644
--- a/Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
+++ b/Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
 import Mathlib.Algebra.ContinuedFractions.Translations
-import Mathlib.Data.Nat.Order.Basic
 
 #align_import algebra.continued_fractions.terminated_stable from "leanprover-community/mathlib"@"a7e36e48519ab281320c4d192da6a7b348ce40ad"
 
diff --git a/Mathlib/Algebra/EuclideanDomain/Instances.lean b/Mathlib/Algebra/EuclideanDomain/Instances.lean
index 88b2e4fd33985..58bc2b4ad6cde 100644
--- a/Mathlib/Algebra/EuclideanDomain/Instances.lean
+++ b/Mathlib/Algebra/EuclideanDomain/Instances.lean
@@ -7,7 +7,6 @@ import Mathlib.Algebra.EuclideanDomain.Defs
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Data.Int.Order.Basic
-import Mathlib.Data.Nat.Order.Basic
 
 #align_import algebra.euclidean_domain.instances from "leanprover-community/mathlib"@"e1bccd6e40ae78370f01659715d3c948716e3b7e"
 
diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean
index 0f66626fd0622..6cdb832f5d1dc 100644
--- a/Mathlib/Algebra/GroupPower/Order.lean
+++ b/Mathlib/Algebra/GroupPower/Order.lean
@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import Mathlib.Algebra.GroupPower.CovariantClass
 import Mathlib.Algebra.GroupPower.Ring
+import Mathlib.Algebra.Order.Ring.Canonical
 
 #align_import algebra.group_power.order from "leanprover-community/mathlib"@"00f91228655eecdcd3ac97a7fd8dbcb139fe990a"
 
@@ -15,6 +16,8 @@ Note that some lemmas are in `Algebra/GroupPower/Lemmas.lean` as they import fil
 depend on this file.
 -/
 
+assert_not_exists Set.range
+
 open Function Int
 
 variable {α M R : Type*}
@@ -209,7 +212,7 @@ theorem pow_le_pow_right (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m := pow_r
 #align pow_le_pow pow_le_pow_right
 
 theorem le_self_pow (ha : 1 ≤ a) (h : m ≠ 0) : a ≤ a ^ m := by
-  simpa only [pow_one] using pow_le_pow_right ha <| pos_iff_ne_zero.2 h
+  simpa only [pow_one] using pow_le_pow_right ha <| Nat.pos_iff_ne_zero.2 h
 #align self_le_pow le_self_pow
 #align le_self_pow le_self_pow
 
@@ -261,6 +264,7 @@ lemma pow_right_strictMono (h : 1 < a) : StrictMono (a ^ ·) :=
 @[gcongr]
 theorem pow_lt_pow_right (h : 1 < a) (hmn : m < n) : a ^ m < a ^ n := pow_right_strictMono h hmn
 #align pow_lt_pow_right pow_lt_pow_right
+#align nat.pow_lt_pow_of_lt_right pow_lt_pow_right
 
 lemma pow_lt_pow_iff_right (h : 1 < a) : a ^ n < a ^ m ↔ n < m := (pow_right_strictMono h).lt_iff_lt
 #align pow_lt_pow_iff_ pow_lt_pow_iff_right
@@ -432,7 +436,7 @@ protected lemma Even.add_pow_le (hn : ∃ k, 2 * k = n) :
         rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
     _ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) := mul_le_mul_of_nonneg_left
           (add_pow_le (sq_nonneg _) (sq_nonneg _) _) $ pow_nonneg (zero_le_two (α := R)) _
-    _ = _ := by simp only [← mul_assoc, ← pow_add, ← pow_mul]; cases n; rfl; simp [two_mul]
+    _ = _ := by simp only [← mul_assoc, ← pow_add, ← pow_mul]; cases n; rfl; simp [Nat.two_mul]
 
 end LinearOrderedSemiring
 
@@ -524,6 +528,20 @@ theorem map_sub_swap (x y : R) : f (x - y) = f (y - x) := by rw [← map_neg, ne
 
 end MonoidHom
 
+namespace Nat
+variable {n : ℕ} {f : α → ℕ}
+
+/-- See also `pow_left_strictMonoOn`. -/
+protected lemma pow_left_strictMono (hn : n ≠ 0) : StrictMono (. ^ n : ℕ → ℕ) :=
+  fun _ _ h ↦ Nat.pow_lt_pow_left h hn
+#align nat.pow_left_strict_mono Nat.pow_left_strictMono
+
+lemma _root_.StrictMono.nat_pow [Preorder α] (hn : n ≠ 0) (hf : StrictMono f) :
+    StrictMono (f · ^ n) := (Nat.pow_left_strictMono hn).comp hf
+#align strict_mono.nat_pow StrictMono.nat_pow
+
+end Nat
+
 /-!
 ### Deprecated lemmas
 
@@ -546,3 +564,9 @@ Those lemmas have been deprecated on 2023-12-23.
 @[deprecated] alias lt_of_pow_lt_pow := lt_of_pow_lt_pow_left
 @[deprecated] alias le_of_pow_le_pow := le_of_pow_le_pow_left
 @[deprecated] alias self_le_pow := le_self_pow
+@[deprecated] alias Nat.pow_lt_pow_of_lt_left := Nat.pow_lt_pow_left
+@[deprecated] alias Nat.pow_le_iff_le_left := Nat.pow_le_pow_iff_left
+@[deprecated] alias Nat.pow_lt_pow_of_lt_right := pow_lt_pow_right
+@[deprecated] protected alias Nat.pow_right_strictMono := pow_right_strictMono
+@[deprecated] alias Nat.pow_le_iff_le_right := pow_le_pow_iff_right
+@[deprecated] alias Nat.pow_lt_iff_lt_right := pow_lt_pow_iff_right
diff --git a/Mathlib/Algebra/GroupPower/Ring.lean b/Mathlib/Algebra/GroupPower/Ring.lean
index 455a6a2d5a746..4f347e5b436df 100644
--- a/Mathlib/Algebra/GroupPower/Ring.lean
+++ b/Mathlib/Algebra/GroupPower/Ring.lean
@@ -8,7 +8,6 @@ import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Ring.Commute
 import Mathlib.Algebra.Ring.Divisibility.Basic
-import Mathlib.Data.Nat.Order.Basic
 
 #align_import algebra.group_power.ring from "leanprover-community/mathlib"@"fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e"
 
diff --git a/Mathlib/Algebra/Order/Floor/Div.lean b/Mathlib/Algebra/Order/Floor/Div.lean
index d0997ef137c7b..a4c5b40cea1c1 100644
--- a/Mathlib/Algebra/Order/Floor/Div.lean
+++ b/Mathlib/Algebra/Order/Floor/Div.lean
@@ -6,7 +6,6 @@ Authors: Yaël Dillies
 import Mathlib.Algebra.Order.Module.Defs
 import Mathlib.Algebra.Order.Pi
 import Mathlib.Data.Finsupp.Order
-import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Order.GaloisConnection
 
 /-!
diff --git a/Mathlib/Combinatorics/Additive/SalemSpencer.lean b/Mathlib/Combinatorics/Additive/SalemSpencer.lean
index 6e96cfb3c5697..9411ce55b7f64 100644
--- a/Mathlib/Combinatorics/Additive/SalemSpencer.lean
+++ b/Mathlib/Combinatorics/Additive/SalemSpencer.lean
@@ -338,8 +338,8 @@ theorem mulRothNumber_le : mulRothNumber s ≤ s.card := Nat.findGreatest_le s.c
 @[to_additive]
 theorem mulRothNumber_spec :
     ∃ (t : _) (_ : t ⊆ s), t.card = mulRothNumber s ∧ MulSalemSpencer (t : Set α) :=
-  @Nat.findGreatest_spec _ _
-    (fun m => ∃ (t : _) (_ : t ⊆ s), t.card = m ∧ MulSalemSpencer (t : Set α)) _ (Nat.zero_le _)
+  Nat.findGreatest_spec
+    (P := fun m => ∃ (t : _) (_ : t ⊆ s), t.card = m ∧ MulSalemSpencer (t : Set α)) (Nat.zero_le _)
     ⟨∅, empty_subset _, card_empty, by norm_cast; exact mulSalemSpencer_empty⟩
 #align mul_roth_number_spec mulRothNumber_spec
 #align add_roth_number_spec addRothNumber_spec
diff --git a/Mathlib/Computability/Ackermann.lean b/Mathlib/Computability/Ackermann.lean
index 8db134ecce020..858dfecbcbe29 100644
--- a/Mathlib/Computability/Ackermann.lean
+++ b/Mathlib/Computability/Ackermann.lean
@@ -6,8 +6,6 @@ Authors: Violeta Hernández Palacios
 import Mathlib.Computability.Primrec
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Linarith
-import Mathlib.Algebra.GroupPower.Order
-import Mathlib.Data.Nat.Pow
 
 #align_import computability.ackermann from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383"
 
diff --git a/Mathlib/Data/BitVec/Defs.lean b/Mathlib/Data/BitVec/Defs.lean
index b5bacec9d4d4a..7ff8f9a2712ca 100644
--- a/Mathlib/Data/BitVec/Defs.lean
+++ b/Mathlib/Data/BitVec/Defs.lean
@@ -3,9 +3,9 @@ Copyright (c) 2015 Joe Hendrix. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Sebastian Ullrich, Harun Khan, Alex Keizer, Abdalrhman M Mohamed
 -/
-
 import Mathlib.Data.Fin.Basic
 import Mathlib.Data.ZMod.Defs
+import Mathlib.Init.Data.Nat.Bitwise
 import Std.Data.BitVec
 
 #align_import data.bitvec.core from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean
index ad8f891812ac6..5785a8011af73 100644
--- a/Mathlib/Data/Fintype/Basic.lean
+++ b/Mathlib/Data/Fintype/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
 -/
+import Mathlib.Algebra.Ring.Hom.Defs -- FIXME: This import is bogus
 import Mathlib.Data.Finset.Image
 import Mathlib.Data.Fin.OrderHom
 
diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
index c6106ca3a55d5..b9248ec8d903e 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -411,20 +411,20 @@ theorem shiftLeft_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (n + k) = (m <<
   | (m : ℕ), n, -[k+1] =>
     subNatNat_elim n k.succ (fun n k i => (↑m) <<< i = (Nat.shiftLeft' false m n) >>> k)
       (fun (i n : ℕ) =>
-        by dsimp; simp [← Nat.shiftLeft_sub _ , add_tsub_cancel_left])
+        by dsimp; simp [← Nat.shiftLeft_sub _ , Nat.add_sub_cancel_left])
       fun i n => by
         dsimp
         simp only [Nat.shiftLeft'_false, Nat.shiftRight_add, le_refl, ← Nat.shiftLeft_sub,
-          tsub_eq_zero_of_le, Nat.shiftLeft_zero]
+          Nat.sub_eq_zero_of_le, Nat.shiftLeft_zero]
         rfl
   | -[m+1], n, -[k+1] =>
     subNatNat_elim n k.succ
       (fun n k i => -[m+1] <<< i = -[(Nat.shiftLeft' true m n) >>> k+1])
       (fun i n =>
         congr_arg negSucc <| by
-          rw [← Nat.shiftLeft'_sub, add_tsub_cancel_left]; apply Nat.le_add_right)
+          rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]; apply Nat.le_add_right)
       fun i n =>
-      congr_arg negSucc <| by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub, tsub_self]
+      congr_arg negSucc <| by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub, Nat.sub_self]
       <;> rfl
 #align int.shiftl_add Int.shiftLeft_add
 
@@ -441,7 +441,7 @@ theorem shiftRight_eq_div_pow : ∀ (m : ℤ) (n : ℕ), m >>> (n : ℤ) = m / (
   | (m : ℕ), n => by rw [shiftRight_coe_nat, Nat.shiftRight_eq_div_pow _ _]; simp
   | -[m+1], n => by
     rw [shiftRight_negSucc, negSucc_ediv, Nat.shiftRight_eq_div_pow]; rfl
-    exact ofNat_lt_ofNat_of_lt (pow_pos (by decide) _)
+    exact ofNat_lt_ofNat_of_lt (Nat.pow_pos (by decide))
 #align int.shiftr_eq_div_pow Int.shiftRight_eq_div_pow
 
 theorem one_shiftLeft (n : ℕ) : 1 <<< (n : ℤ) = (2 ^ n : ℕ) :=
diff --git a/Mathlib/Data/Int/Dvd/Pow.lean b/Mathlib/Data/Int/Dvd/Pow.lean
index deba7a7f6cff8..8737c3b3b2f00 100644
--- a/Mathlib/Data/Int/Dvd/Pow.lean
+++ b/Mathlib/Data/Int/Dvd/Pow.lean
@@ -33,7 +33,7 @@ theorem pow_dvd_of_le_of_pow_dvd {p m n : ℕ} {k : ℤ} (hmn : m ≤ n) (hdiv :
 #align int.pow_dvd_of_le_of_pow_dvd Int.pow_dvd_of_le_of_pow_dvd
 
 theorem dvd_of_pow_dvd {p k : ℕ} {m : ℤ} (hk : 1 ≤ k) (hpk : ↑(p ^ k) ∣ m) : ↑p ∣ m :=
-  (dvd_pow_self _ <| pos_iff_ne_zero.1 hk).natCast.trans hpk
+  (dvd_pow_self _ <| Nat.ne_of_gt hk).natCast.trans hpk
 #align int.dvd_of_pow_dvd Int.dvd_of_pow_dvd
 
 end Int
diff --git a/Mathlib/Data/Int/Order/Lemmas.lean b/Mathlib/Data/Int/Order/Lemmas.lean
index 567f58a174b28..2524c5c6dd7f6 100644
--- a/Mathlib/Data/Int/Order/Lemmas.lean
+++ b/Mathlib/Data/Int/Order/Lemmas.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Data.Nat.Pow
 
 #align_import data.int.order.lemmas from "leanprover-community/mathlib"@"fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e"
 
diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean
index 2f1ee4d4f1771..38d9789a844a5 100644
--- a/Mathlib/Data/List/Perm.lean
+++ b/Mathlib/Data/List/Perm.lean
@@ -615,9 +615,8 @@ theorem Perm.drop_inter {α} [DecidableEq α] {xs ys : List α} (n : ℕ) (h : x
     xs.drop n ~ ys.inter (xs.drop n) := by
   by_cases h'' : n ≤ xs.length
   · let n' := xs.length - n
-    have h₀ : n = xs.length - n' := by
-      rwa [tsub_tsub_cancel_of_le]
-    have h₁ : n' ≤ xs.length := by apply tsub_le_self
+    have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]
+    have h₁ : n' ≤ xs.length := Nat.sub_le ..
     have h₂ : xs.drop n = (xs.reverse.take n').reverse := by
       rw [reverse_take _ h₁, h₀, reverse_reverse]
     rw [h₂]
@@ -627,7 +626,7 @@ theorem Perm.drop_inter {α} [DecidableEq α] {xs ys : List α} (n : ℕ) (h : x
     apply (reverse_perm _).trans; assumption
   · have : drop n xs = [] := by
       apply eq_nil_of_length_eq_zero
-      rw [length_drop, tsub_eq_zero_iff_le]
+      rw [length_drop, Nat.sub_eq_zero_iff_le]
       apply le_of_not_ge h''
     simp [this, List.inter]
 #align list.perm.drop_inter List.Perm.drop_inter
@@ -802,7 +801,7 @@ theorem nthLe_permutations'Aux (s : List α) (x : α) (n : ℕ)
     (hn : n < length (permutations'Aux x s)) :
     (permutations'Aux x s).nthLe n hn = s.insertNth n x := by
   induction' s with y s IH generalizing n
-  · simp only [length, zero_add, lt_one_iff] at hn
+  · simp only [length, zero_add, Nat.lt_one_iff] at hn
     simp [hn]
   · cases n
     · simp [nthLe]
@@ -864,8 +863,7 @@ theorem nodup_permutations'Aux_iff {s : List α} {x : α} : Nodup (permutations'
   intro H
   obtain ⟨k, hk, hk'⟩ := nthLe_of_mem H
   rw [nodup_iff_nthLe_inj] at h
-  suffices k = k + 1 by simp at this
-  refine' h k (k + 1) _ _ _
+  refine k.succ_ne_self.symm $ h k (k + 1) ?_ ?_ ?_
   · simpa [Nat.lt_succ_iff] using hk.le
   · simpa using hk
   rw [nthLe_permutations'Aux, nthLe_permutations'Aux]
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
index 8c618ee81bc4c..5983be75fc98c 100644
--- a/Mathlib/Data/Nat/Basic.lean
+++ b/Mathlib/Data/Nat/Basic.lean
@@ -10,12 +10,25 @@ import Mathlib.Algebra.GroupWithZero.Defs
 #align_import data.nat.basic from "leanprover-community/mathlib"@"bd835ef554f37ef9b804f0903089211f89cb370b"
 
 /-!
-# Basic instances for the natural numbers
+# Algebraic instances for the natural numbers
 
-This file contains:
-* Algebraic instances on the natural numbers
-* Basic lemmas about natural numbers that require more imports than available in
-  `Data.Nat.Defs`.
+This file contains algebraic instances on the natural numbers and a few lemmas about them.
+
+## Implementation note
+
+Std has a home-baked development of the algebraic and order theoretic theory of `ℕ` which, in
+particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness libraries
+in mathlib (naturals show up as indices in lists, cardinality in finsets, powers in groups, ...).
+This home-baked development is pursued in `Data.Nat.Defs`.
+
+Less basic uses of `ℕ` should however use the typeclass-mediated development. This file is the one
+giving access to the algebraic instances. `Data.Nat.Order.Basic` is the one giving access to the
+algebraic order instances.
+
+## TODO
+
+The names of this file, `Data.Nat.Defs` and `Data.Nat.Order.Basic` are archaic and don't match up
+with reality anymore. Rename them.
 -/
 
 open Multiplicative
diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
index adb59a59c105f..be85e6a8749f8 100644
--- a/Mathlib/Data/Nat/Bits.lean
+++ b/Mathlib/Data/Nat/Bits.lean
@@ -7,6 +7,7 @@ import Mathlib.Init.Data.Nat.Bitwise
 import Mathlib.Init.Data.List.Basic
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Data.Nat.Basic
+import Mathlib.Data.Nat.Defs
 import Mathlib.Tactic.Convert
 
 #align_import data.nat.bits from "leanprover-community/mathlib"@"d012cd09a9b256d870751284dd6a29882b0be105"
@@ -28,10 +29,8 @@ and `Nat.digits`.
 set_option linter.deprecated false
 
 namespace Nat
-
 universe u
-
-variable {n : ℕ}
+variable {m n : ℕ}
 
 /-! ### `boddDiv2_eq` and `bodd` -/
 
@@ -160,6 +159,96 @@ theorem bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = fal
     rfl
 #align nat.bit_eq_zero_iff Nat.bit_eq_zero_iff
 
+protected lemma bit0_le (h : n ≤ m) : bit0 n ≤ bit0 m :=
+  add_le_add h h
+#align nat.bit0_le Nat.bit0_le
+
+protected lemma bit1_le {n m : ℕ} (h : n ≤ m) : bit1 n ≤ bit1 m :=
+  succ_le_succ (add_le_add h h)
+#align nat.bit1_le Nat.bit1_le
+
+lemma bit_le : ∀ (b : Bool) {m n : ℕ}, m ≤ n → bit b m ≤ bit b n
+  | true, _, _, h => Nat.bit1_le h
+  | false, _, _, h => Nat.bit0_le h
+#align nat.bit_le Nat.bit_le
+
+lemma bit0_le_bit : ∀ (b) {m n : ℕ}, m ≤ n → bit0 m ≤ bit b n
+  | true, _, _, h => le_of_lt <| Nat.bit0_lt_bit1 h
+  | false, _, _, h => Nat.bit0_le h
+#align nat.bit0_le_bit Nat.bit0_le_bit
+
+lemma bit_le_bit1 : ∀ (b) {m n : ℕ}, m ≤ n → bit b m ≤ bit1 n
+  | false, _, _, h => le_of_lt <| Nat.bit0_lt_bit1 h
+  | true, _, _, h => Nat.bit1_le h
+#align nat.bit_le_bit1 Nat.bit_le_bit1
+
+lemma bit_lt_bit0 : ∀ (b) {m n : ℕ}, m < n → bit b m < bit0 n
+  | true, _, _, h => Nat.bit1_lt_bit0 h
+  | false, _, _, h => Nat.bit0_lt h
+#align nat.bit_lt_bit0 Nat.bit_lt_bit0
+
+protected lemma bit0_lt_bit0 : bit0 m < bit0 n ↔ m < n := by unfold bit0; omega
+
+lemma bit_lt_bit (a b) (h : m < n) : bit a m < bit b n :=
+  lt_of_lt_of_le (bit_lt_bit0 _ h) (bit0_le_bit _ (le_refl _))
+#align nat.bit_lt_bit Nat.bit_lt_bit
+
+@[simp]
+lemma bit0_le_bit1_iff : bit0 m ≤ bit1 n ↔ m ≤ n := by
+  refine ⟨fun h ↦ ?_, fun h ↦ le_of_lt (Nat.bit0_lt_bit1 h)⟩
+  rwa [← Nat.lt_succ_iff, n.bit1_eq_succ_bit0, ← n.bit0_succ_eq, Nat.bit0_lt_bit0, Nat.lt_succ_iff]
+    at h
+#align nat.bit0_le_bit1_iff Nat.bit0_le_bit1_iff
+
+@[simp]
+lemma bit0_lt_bit1_iff : bit0 m < bit1 n ↔ m ≤ n :=
+  ⟨fun h => bit0_le_bit1_iff.1 (le_of_lt h), Nat.bit0_lt_bit1⟩
+#align nat.bit0_lt_bit1_iff Nat.bit0_lt_bit1_iff
+
+@[simp]
+lemma bit1_le_bit0_iff : bit1 m ≤ bit0 n ↔ m < n :=
+  ⟨fun h ↦ by rwa [m.bit1_eq_succ_bit0, Nat.succ_le_iff, Nat.bit0_lt_bit0] at h,
+     fun h ↦ le_of_lt (Nat.bit1_lt_bit0 h)⟩
+#align nat.bit1_le_bit0_iff Nat.bit1_le_bit0_iff
+
+@[simp]
+lemma bit1_lt_bit0_iff : bit1 m < bit0 n ↔ m < n :=
+  ⟨fun h ↦ bit1_le_bit0_iff.1 (le_of_lt h), Nat.bit1_lt_bit0⟩
+#align nat.bit1_lt_bit0_iff Nat.bit1_lt_bit0_iff
+
+-- Porting note: temporarily porting only needed portions
+/-
+@[simp]
+theorem one_le_bit0_iff : 1 ≤ bit0 n ↔ 0 < n := by
+  convert bit1_le_bit0_iff
+  rfl
+#align nat.one_le_bit0_iff Nat.one_le_bit0_iff
+
+@[simp]
+theorem one_lt_bit0_iff : 1 < bit0 n ↔ 1 ≤ n := by
+  convert bit1_lt_bit0_iff
+  rfl
+#align nat.one_lt_bit0_iff Nat.one_lt_bit0_iff
+
+@[simp]
+theorem bit_le_bit_iff : ∀ {b : Bool}, bit b m ≤ bit b n ↔ m ≤ n
+  | false => bit0_le_bit0
+  | true => bit1_le_bit1
+#align nat.bit_le_bit_iff Nat.bit_le_bit_iff
+
+@[simp]
+theorem bit_lt_bit_iff : ∀ {b : Bool}, bit b m < bit b n ↔ m < n
+  | false => bit0_lt_bit0
+  | true => bit1_lt_bit1
+#align nat.bit_lt_bit_iff Nat.bit_lt_bit_iff
+
+@[simp]
+theorem bit_le_bit1_iff : ∀ {b : Bool}, bit b m ≤ bit1 n ↔ m ≤ n
+  | false => bit0_le_bit1_iff
+  | true => bit1_le_bit1
+#align nat.bit_le_bit1_iff Nat.bit_le_bit1_iff
+-/
+
 /--
 The same as `binaryRec_eq`,
 but that one unfortunately requires `f` to be the identity when appending `false` to `0`.
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 629129bed381d..7dda3c0f241a4 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -3,9 +3,10 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Alex Keizer
 -/
-import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Data.List.GetD
 import Mathlib.Data.Nat.Bits
+import Mathlib.Order.Basic
+import Mathlib.Tactic.Common
 
 #align_import data.nat.bitwise from "leanprover-community/mathlib"@"6afc9b06856ad973f6a2619e3e8a0a8d537a58f2"
 
@@ -86,7 +87,7 @@ lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by
   simp only [bit, ite_apply, bit1, bit0, Bool.cond_eq_ite]
   have h1 x :     (x + x) % 2 = 0 := by rw [← two_mul, mul_comm]; apply mul_mod_left
   have h2 x : (x + x + 1) % 2 = 1 := by rw [← two_mul, add_comm]; apply add_mul_mod_self_left
-  have h3 x :     (x + x) / 2 = x := by rw [← two_mul, mul_comm]; apply mul_div_left _ zero_lt_two
+  have h3 x :     (x + x) / 2 = x := by omega
   have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left]
   cases a <;> cases b <;> simp [h1, h2, h3, h4] <;> split_ifs
     <;> simp_all (config := {decide := true})
@@ -245,7 +246,7 @@ theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) :
 theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : testBit m i = true)
     (hnm : ∀ j, i < j → testBit n j = testBit m j) : n < m := by
   induction' n using Nat.binaryRec with b n hn' generalizing i m
-  · rw [pos_iff_ne_zero]
+  · rw [Nat.pos_iff_ne_zero]
     rintro rfl
     simp at hm
   induction' m using Nat.binaryRec with b' m hm' generalizing i
@@ -257,12 +258,12 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
       eq_of_testBit_eq fun i => by convert hnm (i + 1) (Nat.zero_lt_succ _) using 1
       <;> rw [testBit_bit_succ]
     rw [hn, hm, this, bit_false, bit_true, bit0_val, bit1_val]
-    exact lt_add_one _
+    exact Nat.lt_succ_self _
   · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
     simp only [testBit_bit_succ] at hn hm
     have := hn' _ hn hm fun j hj => by
       convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
-    have this' : 2 * n < 2 * m := Nat.mul_lt_mul' (le_refl _) this two_pos
+    have this' : 2 * n < 2 * m := Nat.mul_lt_mul' (le_refl _) this Nat.two_pos
     cases b <;> cases b'
     <;> simp only [bit_false, bit_true, bit0_val n, bit1_val n, bit0_val m, bit1_val m]
     · exact this'
@@ -275,7 +276,7 @@ theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : tes
 
 @[simp]
 theorem testBit_two_pow_self (n : ℕ) : testBit (2 ^ n) n = true := by
-  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n)]
+  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (Nat.pow_pos Nat.zero_lt_two)]
   simp
 #align nat.test_bit_two_pow_self Nat.testBit_two_pow_self
 
@@ -284,8 +285,8 @@ theorem testBit_two_pow_of_ne {n m : ℕ} (hm : n ≠ m) : testBit (2 ^ n) m = f
   cases' hm.lt_or_lt with hm hm
   · rw [Nat.div_eq_of_lt]
     · simp
-    · exact pow_lt_pow_right one_lt_two hm
-  · rw [Nat.pow_div hm.le zero_lt_two, ← tsub_add_cancel_of_le (succ_le_of_lt <| tsub_pos_of_lt hm)]
+    · exact Nat.pow_lt_pow_right Nat.one_lt_two hm
+  · rw [Nat.pow_div hm.le Nat.two_pos, ← Nat.sub_add_cancel (succ_le_of_lt <| Nat.sub_pos_of_lt hm)]
     -- Porting note: XXX why does this make it work?
     rw [(rfl : succ 0 = 1)]
     simp [pow_succ, and_one_is_mod, mul_mod_left]
@@ -459,8 +460,7 @@ theorem lt_xor_cases {a b c : ℕ} (h : a < b ^^^ c) : a ^^^ c < b ∨ a ^^^ b <
 #align nat.lt_lxor_cases Nat.lt_xor_cases
 
 @[simp] theorem bit_lt_two_pow_succ_iff {b x n} : bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n := by
-  rw [pow_succ', ← bit0_eq_two_mul]
-  cases b <;> simp
+  cases b <;> simp [bit0, bit1] <;> omega
 
 /-- If `x` and `y` fit within `n` bits, then the result of any bitwise operation on `x` and `y` also
 fits within `n` bits -/
@@ -480,12 +480,12 @@ theorem bitwise_lt {f x y n} (hx : x < 2 ^ n) (hy : y < 2 ^ n) :
       cases n <;> simp_all
 
 lemma shiftLeft_lt {x n m : ℕ} (h : x < 2 ^ n) : x <<< m < 2 ^ (n + m) := by
-  simp only [pow_add, shiftLeft_eq, mul_lt_mul_right (Nat.two_pow_pos _), h]
+  simp only [Nat.pow_add, shiftLeft_eq, Nat.mul_lt_mul_right (Nat.two_pow_pos _), h]
 
 /-- Note that the LHS is the expression used within `Std.BitVec.append`, hence the name. -/
 lemma append_lt {x y n m} (hx : x < 2 ^ n) (hy : y < 2 ^ m) : y <<< n ||| x < 2 ^ (n + m) := by
   apply bitwise_lt
   · rw [add_comm]; apply shiftLeft_lt hy
-  · apply lt_of_lt_of_le hx <| pow_le_pow_right (le_succ _) (le_add_right _ _)
+  · apply lt_of_lt_of_le hx <| Nat.pow_le_pow_right (le_succ _) (le_add_right _ _)
 
 end Nat
diff --git a/Mathlib/Data/Nat/Choose/Basic.lean b/Mathlib/Data/Nat/Choose/Basic.lean
index 560e1676522d2..3dbded41d96fa 100644
--- a/Mathlib/Data/Nat/Choose/Basic.lean
+++ b/Mathlib/Data/Nat/Choose/Basic.lean
@@ -6,7 +6,6 @@ Authors: Chris Hughes, Bhavik Mehta, Stuart Presnell
 import Mathlib.Data.Nat.Factorial.Basic
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.GroupWithZero.Basic
-import Mathlib.Data.Nat.Order.Basic
 
 #align_import data.nat.choose.basic from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4"
 
@@ -93,7 +92,7 @@ theorem choose_one_right (n : ℕ) : choose n 1 = n := by induction n <;> simp [
 
 -- The `n+1`-st triangle number is `n` more than the `n`-th triangle number
 theorem triangle_succ (n : ℕ) : (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n := by
-  rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, add_tsub_cancel_right, mul_comm]
+  rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, Nat.add_sub_cancel, mul_comm]
   cases n <;> rfl; apply zero_lt_succ
 #align nat.triangle_succ Nat.triangle_succ
 
@@ -108,9 +107,7 @@ theorem choose_two_right (n : ℕ) : choose n 2 = n * (n - 1) / 2 := by
 theorem choose_pos : ∀ {n k}, k ≤ n → 0 < choose n k
   | 0, _, hk => by rw [Nat.eq_zero_of_le_zero hk]; decide
   | n + 1, 0, _ => by simp
-  | n + 1, k + 1, hk => by
-    rw [choose_succ_succ]
-    exact add_pos_of_pos_of_nonneg (choose_pos (le_of_succ_le_succ hk)) (Nat.zero_le _)
+  | n + 1, k + 1, hk => Nat.add_pos_left (choose_pos (le_of_succ_le_succ hk)) _
 #align nat.choose_pos Nat.choose_pos
 
 theorem choose_eq_zero_iff {n k : ℕ} : n.choose k = 0 ↔ n < k :=
@@ -140,10 +137,10 @@ theorem choose_mul_factorial_mul_factorial : ∀ {n k}, k ≤ n → choose n k *
         rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
         simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
       have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
-      rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, add_mul, tsub_mul,
-        factorial_succ, ← add_tsub_assoc_of_le h₃, add_assoc, ← add_mul, add_tsub_cancel_left,
-        add_comm]
-    · rw [hk₁]; simp [hk₁, mul_comm, choose, tsub_self]
+      rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, add_mul,
+        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, add_assoc, ← add_mul,
+        Nat.add_sub_cancel_left, add_comm]
+    · rw [hk₁]; simp [hk₁, mul_comm, choose, Nat.sub_self]
 #align nat.choose_mul_factorial_mul_factorial Nat.choose_mul_factorial_mul_factorial
 
 theorem choose_mul {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) :
@@ -158,26 +155,26 @@ theorem choose_mul {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) :
     _ = n ! :=
       by rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn]
     _ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) :=
-      by rw [choose_mul_factorial_mul_factorial (tsub_le_tsub_right hkn _),
+      by rw [choose_mul_factorial_mul_factorial (Nat.sub_le_sub_right hkn _),
         choose_mul_factorial_mul_factorial (hsk.trans hkn)]
-    _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) :=
-      by rw [tsub_tsub_tsub_cancel_right hsk, mul_assoc, mul_left_comm s !, mul_assoc,
+    _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
+      rw [Nat.sub_sub_sub_cancel_right hsk, mul_assoc, mul_left_comm s !, mul_assoc,
         mul_comm (k - s)!, mul_comm s !, mul_right_comm, ← mul_assoc]
 #align nat.choose_mul Nat.choose_mul
 
 theorem choose_eq_factorial_div_factorial {n k : ℕ} (hk : k ≤ n) :
     choose n k = n ! / (k ! * (n - k)!) := by
   rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]
-  exact (mul_div_left _ (mul_pos (factorial_pos _) (factorial_pos _))).symm
+  exact (mul_div_left _ (Nat.mul_pos (factorial_pos _) (factorial_pos _))).symm
 #align nat.choose_eq_factorial_div_factorial Nat.choose_eq_factorial_div_factorial
 
 theorem add_choose (i j : ℕ) : (i + j).choose j = (i + j)! / (i ! * j !) := by
-  rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), add_tsub_cancel_right, mul_comm]
+  rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right, mul_comm]
 #align nat.add_choose Nat.add_choose
 
 theorem add_choose_mul_factorial_mul_factorial (i j : ℕ) :
     (i + j).choose j * i ! * j ! = (i + j)! := by
-  rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), add_tsub_cancel_right,
+  rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right,
     mul_right_comm]
 #align nat.add_choose_mul_factorial_mul_factorial Nat.add_choose_mul_factorial_mul_factorial
 
@@ -187,19 +184,19 @@ theorem factorial_mul_factorial_dvd_factorial {n k : ℕ} (hk : k ≤ n) : k ! *
 
 theorem factorial_mul_factorial_dvd_factorial_add (i j : ℕ) : i ! * j ! ∣ (i + j)! := by
   suffices i ! * (i + j - i) ! ∣ (i + j)! by
-    rwa [add_tsub_cancel_left i j] at this
+    rwa [Nat.add_sub_cancel_left i j] at this
   exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)
 #align nat.factorial_mul_factorial_dvd_factorial_add Nat.factorial_mul_factorial_dvd_factorial_add
 
 @[simp]
 theorem choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := by
   rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _),
-    tsub_tsub_cancel_of_le hk, mul_comm]
+    Nat.sub_sub_self hk, mul_comm]
 #align nat.choose_symm Nat.choose_symm
 
 theorem choose_symm_of_eq_add {n a b : ℕ} (h : n = a + b) : Nat.choose n a = Nat.choose n b := by
   suffices choose n (n - b) = choose n b by
-    rw [h, add_tsub_cancel_right] at this; rwa [h]
+    rw [h, Nat.add_sub_cancel_right] at this; rwa [h]
   exact choose_symm (h ▸ le_add_left _ _)
 #align nat.choose_symm_of_eq_add Nat.choose_symm_of_eq_add
 
@@ -213,9 +210,9 @@ theorem choose_symm_half (m : ℕ) : choose (2 * m + 1) (m + 1) = choose (2 * m
 #align nat.choose_symm_half Nat.choose_symm_half
 
 theorem choose_succ_right_eq (n k : ℕ) : choose n (k + 1) * (k + 1) = choose n k * (n - k) := by
-  have e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1) := by
-    rw [← right_distrib, ← choose_succ_succ, succ_mul_choose_eq]
-  rw [← tsub_eq_of_eq_add_rev e, mul_comm, ← mul_tsub, add_tsub_add_eq_tsub_right]
+  have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
+    rw [← right_distrib, add_comm (choose _ _), ← choose_succ_succ, succ_mul_choose_eq]
+  rw [← Nat.sub_eq_of_eq_add e, mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]
 #align nat.choose_succ_right_eq Nat.choose_succ_right_eq
 
 @[simp]
@@ -230,7 +227,7 @@ theorem choose_mul_succ_eq (n k : ℕ) : n.choose k * (n + 1) = (n + 1).choose k
   | succ k =>
     obtain hk | hk := le_or_lt (k + 1) (n + 1)
     · rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
-        mul_tsub, add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
+        Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]
     · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul,
         zero_mul]
 #align nat.choose_mul_succ_eq Nat.choose_mul_succ_eq
@@ -239,7 +236,7 @@ theorem ascFactorial_eq_factorial_mul_choose (n k : ℕ) :
     (n + 1).ascFactorial k = k ! * (n + k).choose k := by
   rw [mul_comm]
   apply mul_right_cancel₀ (factorial_ne_zero (n + k - k))
-  rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, add_tsub_cancel_right,
+  rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
     ← factorial_mul_ascFactorial, mul_comm]
 #align nat.asc_factorial_eq_factorial_mul_choose Nat.ascFactorial_eq_factorial_mul_choose
 
@@ -249,7 +246,7 @@ theorem ascFactorial_eq_factorial_mul_choose' (n k : ℕ) :
   · cases k
     · rw [ascFactorial_zero, choose_zero_right, factorial_zero, mul_one]
     · simp only [zero_ascFactorial, zero_eq, zero_add, ge_iff_le, succ_sub_succ_eq_sub,
-        nonpos_iff_eq_zero, tsub_zero, choose_succ_self, mul_zero]
+        Nat.le_zero_eq, Nat.sub_zero, choose_succ_self, mul_zero]
   rw [ascFactorial_eq_factorial_mul_choose]
   simp only [ge_iff_le, succ_add_sub_one]
 
@@ -302,11 +299,11 @@ def fast_choose n k := Nat.descFactorial n k / Nat.factorial k
 /-- Show that `Nat.choose` is increasing for small values of the right argument. -/
 theorem choose_le_succ_of_lt_half_left {r n : ℕ} (h : r < n / 2) :
     choose n r ≤ choose n (r + 1) := by
-  refine' le_of_mul_le_mul_right _ (lt_tsub_iff_left.mpr (lt_of_lt_of_le h (n.div_le_self 2)))
+  refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))
   rw [← choose_succ_right_eq]
   apply Nat.mul_le_mul_left
-  rw [← Nat.lt_iff_add_one_le, lt_tsub_iff_left, ← mul_two]
-  exact lt_of_lt_of_le (mul_lt_mul_of_pos_right h zero_lt_two) (n.div_mul_le_self 2)
+  rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← mul_two]
+  exact lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)
 #align nat.choose_le_succ_of_lt_half_left Nat.choose_le_succ_of_lt_half_left
 
 /-- Show that for small values of the right argument, the middle value is largest. -/
@@ -325,9 +322,9 @@ theorem choose_le_middle (r n : ℕ) : choose n r ≤ choose n (n / 2) := by
     · apply choose_le_middle_of_le_half_left a
     · rw [← choose_symm b]
       apply choose_le_middle_of_le_half_left
-      rw [div_lt_iff_lt_mul' zero_lt_two] at h
-      rw [le_div_iff_mul_le' zero_lt_two, tsub_mul, tsub_le_iff_tsub_le, mul_two,
-        add_tsub_cancel_right]
+      rw [div_lt_iff_lt_mul' Nat.zero_lt_two] at h
+      rw [le_div_iff_mul_le' Nat.zero_lt_two, Nat.mul_sub_right_distrib, Nat.sub_le_iff_le_add,
+        ← Nat.sub_le_iff_le_add', mul_two, Nat.add_sub_cancel]
       exact le_of_lt h
   · rw [choose_eq_zero_of_lt b]
     apply zero_le
@@ -347,7 +344,7 @@ theorem choose_le_add (a b c : ℕ) : choose a c ≤ choose (a + b) c := by
 #align nat.choose_le_add Nat.choose_le_add
 
 theorem choose_le_choose {a b : ℕ} (c : ℕ) (h : a ≤ b) : choose a c ≤ choose b c :=
-  add_tsub_cancel_of_le h ▸ choose_le_add a (b - a) c
+  Nat.add_sub_cancel' h ▸ choose_le_add a (b - a) c
 #align nat.choose_le_choose Nat.choose_le_choose
 
 theorem choose_mono (b : ℕ) : Monotone fun a => choose a b := fun _ _ => choose_le_choose b
@@ -417,8 +414,8 @@ theorem multichoose_eq : ∀ n k : ℕ, multichoose n k = (n + k - 1).choose k
   | _, 0 => by simp
   | 0, k + 1 => by simp
   | n + 1, k + 1 => by
-    have : n + (k + 1) < (n + 1) + (k + 1) := add_lt_add_right (Nat.lt_succ_self _) _
-    have : (n + 1) + k < (n + 1) + (k + 1) := add_lt_add_left (Nat.lt_succ_self _) _
+    have : n + (k + 1) < (n + 1) + (k + 1) := Nat.add_lt_add_right (Nat.lt_succ_self _) _
+    have : (n + 1) + k < (n + 1) + (k + 1) := Nat.add_lt_add_left (Nat.lt_succ_self _) _
     erw [multichoose_succ_succ, add_comm, Nat.succ_add_sub_one, ← add_assoc, Nat.choose_succ_succ]
     simp [multichoose_eq n (k+1), multichoose_eq (n+1) k]
   termination_by a b => a + b
diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean
index cb3e06ceb1ea4..2ee23e9f79eb8 100644
--- a/Mathlib/Data/Nat/Defs.lean
+++ b/Mathlib/Data/Nat/Defs.lean
@@ -25,10 +25,21 @@ This file contains:
   * `strong_rec'`: recursion based on strong inequalities
 * decidability instances on predicates about the natural numbers
 
-Many theorems that used to live in this file have been moved to `Data.Nat.Order`, so that
-this file requires fewer imports. For each section here there is a corresponding section in
-that file with additional results. It may be possible to move some of these results here,
-by tweaking their proofs.
+## Implementation note
+
+Std has a home-baked development of the algebraic and order theoretic theory of `ℕ` which, in
+particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness libraries
+in mathlib (naturals show up as indices in lists, cardinality in finsets, powers in groups, ...).
+This home-baked development is pursued in this file.
+
+Less basic uses of `ℕ` should however use the typeclass-mediated development. `Data.Nat.Basic` gives
+access to the algebraic instances. `Data.Nat.Order.Basic` is the one giving access to the algebraic
+order instances.
+
+## TODO
+
+The names of this file, `Data.Nat.Basic` and `Data.Nat.Order.Basic` are archaic and don't match up
+with reality anymore. Rename them.
 -/
 
 open Function
@@ -132,9 +143,21 @@ lemma one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠
 
 lemma le_one_iff_eq_zero_or_eq_one : ∀ {n : ℕ}, n ≤ 1 ↔ n = 0 ∨ n = 1 := by simp [le_succ_iff]
 
+@[simp] lemma lt_one_iff : n < 1 ↔ n = 0 := Nat.lt_succ_iff.trans $ by rw [le_zero_eq]
+#align nat.lt_one_iff Nat.lt_one_iff
+
+lemma one_le_of_lt (h : a < b) : 1 ≤ b := lt_of_le_of_lt (Nat.zero_le _) h
+#align nat.one_le_of_lt Nat.one_le_of_lt
+
+@[simp] lemma min_eq_zero_iff : min m n = 0 ↔ m = 0 ∨ n = 0 := by omega
+@[simp] lemma max_eq_zero_iff : max m n = 0 ↔ m = 0 ∧ n = 0 := by omega
+#align nat.min_eq_zero_iff Nat.min_eq_zero_iff
+#align nat.max_eq_zero_iff Nat.max_eq_zero_iff
+
 -- Moved to Std
 #align nat.succ_eq_one_add Nat.succ_eq_one_add
 #align nat.one_add Nat.one_add
+#align nat.zero_max Nat.zero_max
 
 lemma pred_eq_sub_one (n : ℕ) : pred n = n - 1 := rfl
 #align nat.pred_eq_sub_one Nat.pred_eq_sub_one
@@ -206,24 +229,127 @@ lemma sub_one_add_self (n : ℕ) : (n - 1) + n = 2 * n - 1 := Nat.add_comm _ n 
 lemma self_add_pred (n : ℕ) : n + pred n = (2 * n).pred := self_add_sub_one n
 lemma pred_add_self (n : ℕ) : pred n + n = (2 * n).pred := sub_one_add_self n
 
+lemma pred_le_iff : pred m ≤ n ↔ m ≤ succ n :=
+  ⟨le_succ_of_pred_le, by cases m; exacts [fun _ ↦ zero_le n, le_of_succ_le_succ]⟩
+#align nat.pred_le_iff Nat.pred_le_iff
+
+lemma lt_of_lt_pred (h : m < n - 1) : m < n := by omega
+#align nat.lt_of_lt_pred Nat.lt_of_lt_pred
+
+lemma le_add_pred_of_pos (a : ℕ) (hb : b ≠ 0) : a ≤ b + (a - 1) := by omega
+#align nat.le_add_pred_of_pos Nat.le_add_pred_of_pos
+
 /-! ### `add` -/
 
+#align nat.add_pos_left Nat.add_pos_left
+#align nat.add_pos_right Nat.add_pos_right
+#align nat.exists_eq_add_of_le Nat.exists_eq_add_of_le
+#align nat.exists_eq_add_of_le' Nat.exists_eq_add_of_le'
+#align nat.exists_eq_add_of_lt Nat.exists_eq_add_of_lt
+
+attribute [simp] le_add_left le_add_right Nat.lt_add_left_iff_pos Nat.lt_add_right_iff_pos
+  Nat.add_le_add_iff_left Nat.add_le_add_iff_right Nat.add_lt_add_iff_left Nat.add_lt_add_iff_right
+  not_lt_zero
+
+-- We want to use these two lemmas earlier than the lemmas simp can prove them with
+@[simp, nolint simpNF] protected alias add_left_inj := Nat.add_right_cancel_iff
+@[simp, nolint simpNF] protected alias add_right_inj := Nat.add_left_cancel_iff
+
 -- Sometimes a bare `Nat.add` or similar appears as a consequence of unfolding during pattern
 -- matching. These lemmas package them back up as typeclass mediated operations.
 @[simp] lemma add_def : Nat.add m n = m + n := rfl
 #align nat.add_def Nat.add_def
 
-#align nat.exists_eq_add_of_le Nat.exists_eq_add_of_le
-#align nat.exists_eq_add_of_le' Nat.exists_eq_add_of_le'
-#align nat.exists_eq_add_of_lt Nat.exists_eq_add_of_lt
+lemma two_le_iff : ∀ n, 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
+  | 0 => by simp
+  | 1 => by simp
+  | n + 2 => by simp
+#align nat.two_le_iff Nat.two_le_iff
+
+lemma add_eq_max_iff : m + n = max m n ↔ m = 0 ∨ n = 0 := by omega
+lemma add_eq_min_iff : m + n = min m n ↔ m = 0 ∧ n = 0 := by omega
+#align nat.add_eq_max_iff Nat.add_eq_max_iff
+#align nat.add_eq_min_iff Nat.add_eq_min_iff
+
+-- We want to use this lemma earlier than the lemma simp can prove it with
+@[simp, nolint simpNF] protected lemma add_eq_zero : m + n = 0 ↔ m = 0 ∧ n = 0 := by omega
+
+lemma add_pos_iff_pos_or_pos : 0 < m + n ↔ 0 < m ∨ 0 < n := by omega
+#align nat.add_pos_iff_pos_or_pos Nat.add_pos_iff_pos_or_pos
+
+lemma add_eq_one_iff : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 := by
+  cases n <;> simp [succ_eq_add_one, ← Nat.add_assoc, succ_inj']
+#align nat.add_eq_one_iff Nat.add_eq_one_iff
+
+lemma add_eq_two_iff : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0 := by
+  omega
+#align nat.add_eq_two_iff Nat.add_eq_two_iff
+
+lemma add_eq_three_iff :
+    m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0 := by
+  omega
+#align nat.add_eq_three_iff Nat.add_eq_three_iff
+
+lemma le_add_one_iff : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1 := by
+  rw [le_iff_lt_or_eq, lt_add_one_iff]
+#align nat.le_add_one_iff Nat.le_add_one_iff
+
+lemma le_and_le_add_one_iff : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1 := by
+  rw [le_add_one_iff, and_or_left, ← le_antisymm_iff, eq_comm, and_iff_right_of_imp]
+  rintro rfl
+  exact n.le_succ
+#align nat.le_and_le_add_one_iff Nat.le_and_le_add_one_iff
+
+lemma add_succ_lt_add (hab : a < b) (hcd : c < d) : a + c + 1 < b + d := by
+  rw [Nat.add_assoc]; exact Nat.add_lt_add_of_lt_of_le hab (Nat.succ_le_iff.2 hcd)
+#align nat.add_succ_lt_add Nat.add_succ_lt_add
+
+theorem le_or_le_of_add_eq_add_pred (h : a + c = b + d - 1) : b ≤ a ∨ d ≤ c := by
+  rcases le_or_lt b a with h' | h' <;> [left; right]
+  · exact h'
+  · replace h' := Nat.add_lt_add_right h' c
+    rw [h] at h'
+    rcases d.eq_zero_or_pos with hn | hn
+    · rw [hn]
+      exact zero_le c
+    rw [d.add_sub_assoc (Nat.succ_le_of_lt hn), Nat.add_lt_add_iff_left] at h'
+    exact Nat.le_of_pred_lt h'
+#align nat.le_or_le_of_add_eq_add_pred Nat.le_or_le_of_add_eq_add_pred
+
+/-! ### `sub` -/
+
+/-- A version of `Nat.sub_succ` in the form `_ - 1` instead of `Nat.pred _`. -/
+lemma sub_succ' (m n : ℕ) : m - n.succ = m - n - 1 := rfl
+#align nat.sub_succ' Nat.sub_succ'
+
+protected lemma lt_sub_iff_add_lt : a < c - b ↔ a + b < c := ⟨add_lt_of_lt_sub, lt_sub_of_add_lt⟩
+protected lemma lt_sub_iff_add_lt' : a < c - b ↔ b + a < c := by omega
+protected lemma sub_lt_iff_lt_add (hba : b ≤ a) : a - b < c ↔ a < b + c := by omega
+protected lemma sub_lt_iff_lt_add' (hba : b ≤ a) : a - b < c ↔ a < c + b := by omega
+
+protected lemma sub_sub_sub_cancel_right (h : c ≤ b) : a - c - (b - c) = a - b := by omega
+protected lemma add_sub_sub_cancel (h : c ≤ a) : a + b - (a - c) = b + c := by omega
+protected lemma sub_add_sub_cancel (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c := by omega
+
+lemma lt_pred_iff : a < pred b ↔ succ a < b := Nat.lt_sub_iff_add_lt (b := 1)
+#align nat.lt_pred_iff Nat.lt_pred_iff
+
+protected lemma sub_lt_sub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b := by omega
 
 /-! ### `mul` -/
 
+#align nat.mul_ne_zero Nat.mul_ne_zero
+#align nat.mul_eq_zero Nat.mul_eq_zero
+#align nat.eq_of_mul_eq_mul_right Nat.eq_of_mul_eq_mul_right
+#align nat.le_mul_of_pos_left Nat.le_mul_of_pos_left
+#align nat.le_mul_of_pos_right Nat.le_mul_of_pos_right
+
 @[simp] lemma mul_def : Nat.mul m n = m * n := rfl
 #align nat.mul_def Nat.mul_def
 
--- Moved to core
-#align nat.eq_of_mul_eq_mul_right Nat.eq_of_mul_eq_mul_right
+-- Porting note: removing `simp` attribute
+protected lemma zero_eq_mul : 0 = m * n ↔ m = 0 ∨ n = 0 := by rw [eq_comm, Nat.mul_eq_zero]
+#align nat.zero_eq_mul Nat.zero_eq_mul
 
 lemma two_mul_ne_two_mul_add_one : 2 * n ≠ 2 * m + 1 :=
   mt (congr_arg (· % 2))
@@ -254,6 +380,9 @@ lemma mul_right_eq_self_iff (ha : 0 < a) : a * b = a ↔ b = 1 := mul_eq_left $
 lemma mul_left_eq_self_iff (hb : 0 < b) : a * b = b ↔ a = 1 := mul_eq_right $ ne_of_gt hb
 #align nat.mul_left_eq_self_iff Nat.mul_left_eq_self_iff
 
+protected lemma le_of_mul_le_mul_right (h : a * c ≤ b * c) (hc : 0 < c) : a ≤ b :=
+  Nat.le_of_mul_le_mul_left (by simpa [Nat.mul_comm]) hc
+
 set_option push_neg.use_distrib true in
 /-- The product of two natural numbers is greater than 1 if and only if
   at least one of them is greater than 1 and both are positive. -/
@@ -268,8 +397,75 @@ lemma one_lt_mul_iff : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n) := by
     · exact Nat.mul_lt_mul_of_lt_of_le' hm h.2.1 Nat.zero_lt_one
     · exact Nat.mul_lt_mul_of_le_of_lt h.1 hn h.1
 
+lemma eq_one_of_mul_eq_one_right (H : m * n = 1) : m = 1 := eq_one_of_dvd_one ⟨n, H.symm⟩
+#align nat.eq_one_of_mul_eq_one_right Nat.eq_one_of_mul_eq_one_right
+
+lemma eq_one_of_mul_eq_one_left (H : m * n = 1) : n = 1 :=
+  eq_one_of_mul_eq_one_right (by rwa [Nat.mul_comm])
+#align nat.eq_one_of_mul_eq_one_left Nat.eq_one_of_mul_eq_one_left
+
+@[simp] protected lemma lt_mul_iff_one_lt_left (hb : 0 < b) : b < a * b ↔ 1 < a := by
+  simpa using Nat.mul_lt_mul_right (b := 1) hb
+
+@[simp] protected lemma lt_mul_iff_one_lt_right (ha : 0 < a) : a < a * b ↔ 1 < b := by
+  simpa using Nat.mul_lt_mul_left (b := 1) ha
+
+lemma eq_zero_of_double_le (h : 2 * n ≤ n) : n = 0 := by omega
+#align nat.eq_zero_of_double_le Nat.eq_zero_of_double_le
+
+lemma eq_zero_of_mul_le (hb : 2 ≤ n) (h : n * m ≤ m) : m = 0 :=
+  eq_zero_of_double_le <| le_trans (Nat.mul_le_mul_right _ hb) h
+#align nat.eq_zero_of_mul_le Nat.eq_zero_of_mul_le
+
+lemma succ_mul_pos (m : ℕ) (hn : 0 < n) : 0 < succ m * n := Nat.mul_pos m.succ_pos hn
+#align nat.succ_mul_pos Nat.succ_mul_pos
+
+lemma mul_self_le_mul_self (h : m ≤ n) : m * m ≤ n * n := Nat.mul_le_mul h h
+#align nat.mul_self_le_mul_self Nat.mul_self_le_mul_self
+
+lemma mul_lt_mul'' (hac : a < c) (hbd : b < d) : a * b < c * d :=
+  Nat.mul_lt_mul_of_lt_of_le hac (le_of_lt hbd) $ by omega
+
+lemma mul_self_lt_mul_self (h : m < n) : m * m < n * n := mul_lt_mul'' h h
+#align nat.mul_self_lt_mul_self Nat.mul_self_lt_mul_self
+
+lemma mul_self_le_mul_self_iff : m * m ≤ n * n ↔ m ≤ n :=
+  ⟨le_imp_le_of_lt_imp_lt mul_self_lt_mul_self, mul_self_le_mul_self⟩
+#align nat.mul_self_le_mul_self_iff Nat.mul_self_le_mul_self_iff
+
+lemma mul_self_lt_mul_self_iff : m * m < n * n ↔ m < n := by
+  simp only [← not_le, mul_self_le_mul_self_iff]
+#align nat.mul_self_lt_mul_self_iff Nat.mul_self_lt_mul_self_iff
+
+lemma le_mul_self : ∀ n : ℕ, n ≤ n * n
+  | 0 => le_refl _
+  | n + 1 => by simp [Nat.mul_add]
+#align nat.le_mul_self Nat.le_mul_self
+
+lemma mul_self_inj : m * m = n * n ↔ m = n := by simp [le_antisymm_iff, mul_self_le_mul_self_iff]
+#align nat.mul_self_inj Nat.mul_self_inj
+
+@[simp] lemma lt_mul_self_iff : ∀ {n : ℕ}, n < n * n ↔ 1 < n
+  | 0 => by simp
+  | n + 1 => Nat.lt_mul_iff_one_lt_left n.succ_pos
+#align nat.lt_mul_self_iff Nat.lt_mul_self_iff
+
+lemma add_sub_one_le_mul (ha : a ≠ 0) (hb : b ≠ 0) : a + b - 1 ≤ a * b := by
+  cases a
+  · cases ha rfl
+  · rw [succ_add, Nat.add_one_sub_one, succ_mul]
+    exact Nat.add_le_add_right (Nat.le_mul_of_pos_right _ $ Nat.pos_iff_ne_zero.2 hb) _
+#align nat.add_sub_one_le_mul Nat.add_sub_one_le_mul
+
+protected lemma add_le_mul {a : ℕ} (ha : 2 ≤ a) : ∀ {b : ℕ} (_ : 2 ≤ b), a + b ≤ a * b
+  | 2, _ => by omega
+  | b + 3, _ => by have := Nat.add_le_mul ha (Nat.le_add_left _ b); rw [mul_succ]; omega
+
 /-! ### `div` -/
 
+#align nat.pow_div Nat.pow_div
+#align nat.div_lt_of_lt_mul Nat.div_lt_of_lt_mul
+
 attribute [simp] Nat.div_self
 
 lemma div_le_iff_le_mul_add_pred (hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1) := by
@@ -358,6 +554,192 @@ lemma div_mul_div_comm : b ∣ a → d ∣ c → (a / b) * (c / d) = (a * c) / (
     Nat.mul_left_comm x, ← Nat.mul_assoc b, Nat.mul_div_cancel_left _ (Nat.mul_pos hb hd)]
 #align nat.div_mul_div_comm Nat.div_mul_div_comm
 
+lemma eq_zero_of_le_div (hn : 2 ≤ n) (h : m ≤ m / n) : m = 0 :=
+  eq_zero_of_mul_le hn <| by
+    rw [Nat.mul_comm]; exact (Nat.le_div_iff_mul_le' (lt_of_lt_of_le (by decide) hn)).1 h
+#align nat.eq_zero_of_le_div Nat.eq_zero_of_le_div
+
+lemma div_mul_div_le_div (a b c : ℕ) : a / c * b / a ≤ b / c := by
+  obtain rfl | ha := eq_or_ne a 0
+  · simp
+  · calc
+      a / c * b / a ≤ b * a / c / a :=
+        Nat.div_le_div_right (by rw [Nat.mul_comm]; exact mul_div_le_mul_div_assoc _ _ _)
+      _ = b / c := by rw [Nat.div_div_eq_div_mul, Nat.mul_comm b, Nat.mul_comm c,
+          Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero ha)]
+#align nat.div_mul_div_le_div Nat.div_mul_div_le_div
+
+lemma eq_zero_of_le_half (h : n ≤ n / 2) : n = 0 := eq_zero_of_le_div (le_refl _) h
+#align nat.eq_zero_of_le_half Nat.eq_zero_of_le_half
+
+lemma le_half_of_half_lt_sub (h : a / 2 < a - b) : b ≤ a / 2 := by
+  rw [Nat.le_div_iff_mul_le Nat.two_pos]
+  rw [Nat.div_lt_iff_lt_mul Nat.two_pos, Nat.mul_sub_right_distrib, Nat.lt_sub_iff_add_lt,
+    Nat.mul_two a] at h
+  exact le_of_lt (Nat.lt_of_add_lt_add_left h)
+#align nat.le_half_of_half_lt_sub Nat.le_half_of_half_lt_sub
+
+lemma half_le_of_sub_le_half (h : a - b ≤ a / 2) : a / 2 ≤ b := by
+  rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.mul_sub_right_distrib, Nat.sub_le_iff_le_add,
+    Nat.mul_two, Nat.add_le_add_iff_left] at h
+  rw [← Nat.mul_div_left b Nat.two_pos]
+  exact Nat.div_le_div_right h
+#align nat.half_le_of_sub_le_half Nat.half_le_of_sub_le_half
+
+protected lemma div_le_of_le_mul' (h : m ≤ k * n) : m / k ≤ n := by
+  obtain rfl | hk := k.eq_zero_or_pos
+  · simp
+  · refine Nat.le_of_mul_le_mul_left ?_ hk
+    calc
+      k * (m / k) ≤ m % k + k * (m / k) := Nat.le_add_left _ _
+      _ = m := mod_add_div _ _
+      _ ≤ k * n := h
+#align nat.div_le_of_le_mul' Nat.div_le_of_le_mul'
+
+protected lemma div_le_self' (m n : ℕ) : m / n ≤ m := by
+  obtain rfl | hn := n.eq_zero_or_pos
+  · simp
+  · refine Nat.div_le_of_le_mul' ?_
+    calc
+      m = 1 * m := by rw [Nat.one_mul]
+      _ ≤ n * m := Nat.mul_le_mul_right _ hn
+#align nat.div_le_self' Nat.div_le_self'
+
+lemma two_mul_odd_div_two (hn : n % 2 = 1) : 2 * (n / 2) = n - 1 := by
+  conv => rhs; rw [← Nat.mod_add_div n 2, hn, Nat.add_sub_cancel_left]
+#align nat.two_mul_odd_div_two Nat.two_mul_odd_div_two
+
+@[gcongr]
+lemma div_le_div_left (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c :=
+  (Nat.le_div_iff_mul_le hc).2 <| le_trans (Nat.mul_le_mul_left _ hcb) (div_mul_le_self _ _)
+#align nat.div_le_div_left Nat.div_le_div_left
+
+lemma div_eq_self : m / n = m ↔ m = 0 ∨ n = 1 := by
+  constructor
+  · intro
+    match n with
+    | 0 => simp_all
+    | 1 => right; rfl
+    | n+2 =>
+      left
+      have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)
+      refine eq_zero_of_le_half ?_
+      simp_all
+  · rintro (rfl | rfl) <;> simp
+#align nat.div_eq_self Nat.div_eq_self
+
+lemma div_eq_sub_mod_div : m / n = (m - m % n) / n := by
+  obtain rfl | hn := n.eq_zero_or_pos
+  · rw [Nat.div_zero, Nat.div_zero]
+  · have : m - m % n = n * (m / n) := by
+      rw [Nat.sub_eq_iff_eq_add (Nat.mod_le _ _), Nat.add_comm, mod_add_div]
+    rw [this, mul_div_right _ hn]
+#align nat.div_eq_sub_mod_div Nat.div_eq_sub_mod_div
+
+/-!
+### `pow`
+
+#### TODO
+
+* Rename `Nat.pow_le_pow_of_le_left` to `Nat.pow_le_pow_left`, protect it, remove the alias
+* Rename `Nat.pow_le_pow_of_le_right` to `Nat.pow_le_pow_right`, protect it, remove the alias
+-/
+
+#align nat.pow_le_pow_of_le_left Nat.pow_le_pow_left
+#align nat.pow_le_pow_of_le_right Nat.pow_le_pow_right
+#align nat.pow_le_iff_lt_right Nat.pow_le_pow_iff_right
+#align nat.pow_lt_iff_lt_right Nat.pow_lt_pow_iff_right
+#align nat.pow_lt_pow_succ Nat.pow_lt_pow_succ
+
+protected lemma pow_lt_pow_left (h : a < b) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
+  | 1, _ => by simpa
+  | n + 2, _ => Nat.mul_lt_mul_of_lt_of_le (Nat.pow_lt_pow_left h n.succ_ne_zero) (Nat.le_of_lt h)
+    (zero_lt_of_lt h)
+#align nat.pow_lt_pow_of_lt_left Nat.pow_lt_pow_left
+
+protected lemma pow_lt_pow_right (ha : 1 < a) (h : m < n) : a ^ m < a ^ n :=
+  (Nat.pow_lt_pow_iff_right ha).2 h
+
+protected lemma pow_le_pow_iff_left {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b where
+  mp := by simpa only [← Nat.not_le, not_imp_not] using (Nat.pow_lt_pow_left · hn)
+  mpr h := Nat.pow_le_pow_left h _
+#align nat.pow_le_iff_le_left Nat.pow_le_pow_iff_left
+
+protected lemma pow_lt_pow_iff_left (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b := by
+  simp only [← Nat.not_le, Nat.pow_le_pow_iff_left hn]
+#align nat.pow_lt_iff_lt_left Nat.pow_lt_pow_iff_left
+
+lemma pow_left_injective (hn : n ≠ 0) : Injective (fun a : ℕ ↦ a ^ n) := by
+  simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_left hn]
+#align nat.pow_left_injective Nat.pow_left_injective
+
+protected lemma pow_right_injective (ha : 2 ≤ a) : Injective (a ^ ·) :=by
+  simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_right ha]
+#align nat.pow_right_injective Nat.pow_right_injective
+
+-- We want to use this lemma earlier than the lemma simp can prove it with
+@[simp, nolint simpNF] protected lemma pow_eq_zero {a : ℕ} : ∀ {n : ℕ}, a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
+  | 0 => by simp
+  | n + 1 => by rw [Nat.pow_succ, mul_eq_zero, Nat.pow_eq_zero]; omega
+
+lemma le_self_pow (hn : n ≠ 0) : ∀ a : ℕ, a ≤ a ^ n
+  | 0 => zero_le _
+  | a + 1 => by simpa using Nat.pow_le_pow_right a.succ_pos (Nat.one_le_iff_ne_zero.2 hn)
+#align nat.le_self_pow Nat.le_self_pow
+
+lemma lt_pow_self (ha : 1 < a) : ∀ n : ℕ, n < a ^ n
+  | 0 => by simp
+  | n + 1 =>
+    calc
+      n + 1 < a ^ n + 1 := Nat.add_lt_add_right (lt_pow_self ha _) _
+      _ ≤ a ^ (n + 1) := Nat.pow_lt_pow_succ ha
+#align nat.lt_pow_self Nat.lt_pow_self
+
+lemma lt_two_pow (n : ℕ) : n < 2 ^ n := lt_pow_self (by decide) n
+#align nat.lt_two_pow Nat.lt_two_pow
+
+lemma one_le_pow (n m : ℕ) (h : 0 < m) : 1 ≤ m ^ n := by simpa using Nat.pow_le_pow_of_le_left h n
+#align nat.one_le_pow Nat.one_le_pow
+
+lemma one_le_pow' (n m : ℕ) : 1 ≤ (m + 1) ^ n := one_le_pow n (m + 1) (succ_pos m)
+#align nat.one_le_pow' Nat.one_le_pow'
+
+#align nat.one_le_two_pow Nat.one_le_two_pow
+
+lemma one_lt_pow (hn : n ≠ 0) (ha : 1 < a) : 1 < a ^ n := by simpa using Nat.pow_lt_pow_left ha hn
+#align nat.one_lt_pow Nat.one_lt_pow
+
+lemma two_pow_succ (n : ℕ) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n := by simp [Nat.pow_succ, Nat.mul_two]
+
+lemma one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) :=
+  one_lt_pow n.succ_ne_zero (Nat.lt_of_sub_eq_succ rfl)
+#align nat.one_lt_pow' Nat.one_lt_pow'
+
+@[simp] lemma one_lt_pow_iff {n : ℕ} (hn : n ≠ 0) : ∀ {a}, 1 < a ^ n ↔ 1 < a
+ | 0 => by simp [Nat.zero_pow (Nat.pos_of_ne_zero hn)]
+ | 1 => by simp
+ | a + 2 => by simp [one_lt_pow hn]
+  -- one_lt_pow_iff_of_nonneg (zero_le _) h
+#align nat.one_lt_pow_iff Nat.one_lt_pow_iff
+
+#align nat.one_lt_two_pow Nat.one_lt_two_pow
+
+lemma one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1) := one_lt_pow n.succ_ne_zero (by decide)
+#align nat.one_lt_two_pow' Nat.one_lt_two_pow'
+
+lemma mul_lt_mul_pow_succ (ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1) := by
+  rw [Nat.pow_succ, ← Nat.mul_assoc, Nat.mul_lt_mul_right (lt_trans Nat.zero_lt_one hb)]
+  exact Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_left _ ha)
+    ((Nat.mul_lt_mul_left ha).2 $ Nat.lt_pow_self hb _)
+#align nat.mul_lt_mul_pow_succ Nat.mul_lt_mul_pow_succ
+
+lemma sq_sub_sq (a b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
+  simpa [Nat.pow_succ] using Nat.mul_self_sub_mul_self_eq a b
+#align nat.sq_sub_sq Nat.sq_sub_sq
+
+alias pow_two_sub_pow_two := sq_sub_sq
+#align nat.pow_two_sub_pow_two Nat.pow_two_sub_pow_two
+
 protected lemma div_pow (h : a ∣ b) : (b / a) ^ c = b ^ c / a ^ c := by
   obtain rfl | hc := c.eq_zero_or_pos
   · simp
@@ -567,8 +949,103 @@ def decreasingInduction' {P : ℕ → Sort*} {m n : ℕ} (h : ∀ k < n, m ≤ k
     exact hP
 #align nat.decreasing_induction' Nat.decreasingInduction'
 
+/-- Given a predicate on two naturals `P : ℕ → ℕ → Prop`, `P a b` is true for all `a < b` if
+`P (a + 1) (a + 1)` is true for all `a`, `P 0 (b + 1)` is true for all `b` and for all
+`a < b`, `P (a + 1) b` is true and `P a (b + 1)` is true implies `P (a + 1) (b + 1)` is true. -/
+@[elab_as_elim]
+theorem diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ a, P (a + 1) (a + 1)) (hb : ∀ b, P 0 (b + 1))
+    (hd : ∀ a b, a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) : ∀ a b, a < b → P a b
+  | 0, b + 1, _ => hb _
+  | a + 1, b + 1, h => by
+    apply hd _ _ (Nat.add_lt_add_iff_right.1 h)
+    · have this : a + 1 = b ∨ a + 1 < b := by omega
+      have wf : (a + 1) + b < (a + 1) + (b + 1) := by simp
+      rcases this with (rfl | h)
+      · exact ha _
+      apply diag_induction P ha hb hd (a + 1) b h
+    have _ : a + (b + 1) < (a + 1) + (b + 1) := by simp
+    apply diag_induction P ha hb hd a (b + 1)
+    apply lt_of_le_of_lt (Nat.le_succ _) h
+  termination_by a b _c => a + b
+  decreasing_by all_goals assumption
+#align nat.diag_induction Nat.diag_induction
+
+/-- A subset of `ℕ` containing `k : ℕ` and closed under `Nat.succ` contains every `n ≥ k`. -/
+lemma set_induction_bounded {S : Set ℕ} (hk : k ∈ S) (h_ind : ∀ k : ℕ, k ∈ S → k + 1 ∈ S)
+    (hnk : k ≤ n) : n ∈ S :=
+  @leRecOn (fun n => n ∈ S) k n hnk @h_ind hk
+#align nat.set_induction_bounded Nat.set_induction_bounded
+
+/-- A subset of `ℕ` containing zero and closed under `Nat.succ` contains all of `ℕ`. -/
+lemma set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ k : ℕ, k ∈ S → k + 1 ∈ S) (n : ℕ) :
+    n ∈ S :=
+  set_induction_bounded hb h_ind (zero_le n)
+#align nat.set_induction Nat.set_induction
+
 /-! ### `mod`, `dvd` -/
 
+#align nat.pow_dvd_of_le_of_pow_dvd Nat.pow_dvd_of_le_of_pow_dvd
+#align nat.dvd_of_pow_dvd Nat.dvd_of_pow_dvd
+#align nat.mod_pow_succ Nat.mod_pow_succ
+#align nat.pow_dvd_pow_iff_pow_le_pow Nat.pow_dvd_pow_iff_pow_le_pow
+#align nat.pow_dvd_pow_iff_le_right Nat.pow_dvd_pow_iff_le_right
+#align nat.pow_dvd_pow_iff_le_right' Nat.pow_dvd_pow_iff_le_right'
+#align nat.mod_mul_right_div_self Nat.mod_mul_right_div_self
+#align nat.mod_mul_left_div_self Nat.mod_mul_left_div_self
+
+lemma mul_div_mul_comm_of_dvd_dvd (hba : b ∣ a) (hdc : d ∣ c) :
+    a * c / (b * d) = a / b * (c / d) := by
+  obtain rfl | hb := b.eq_zero_or_pos; · simp
+  obtain rfl | hd := d.eq_zero_or_pos; · simp
+  obtain ⟨_, rfl⟩ := hba
+  obtain ⟨_, rfl⟩ := hdc
+  rw [Nat.mul_mul_mul_comm, Nat.mul_div_cancel_left _ hb, Nat.mul_div_cancel_left _ hd,
+    Nat.mul_div_cancel_left _ (Nat.mul_pos hb hd)]
+#align nat.mul_div_mul_comm_of_dvd_dvd Nat.mul_div_mul_comm_of_dvd_dvd
+
+@[simp] lemma mul_mod_mod (a b c : ℕ) : (a * (b % c)) % c = a * b % c := by
+  rw [mul_mod, mod_mod, ← mul_mod]
+
+@[simp] lemma mod_mul_mod (a b c : ℕ) : (a % c * b) % c = a * b % c := by
+  rw [mul_mod, mod_mod, ← mul_mod]
+
+lemma pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n := by
+  induction' b with b ih; rfl; simp [Nat.pow_succ, Nat.mul_mod, ih]
+#align nat.pow_mod Nat.pow_mod
+
+lemma not_pos_pow_dvd : ∀ {a n : ℕ} (_ : 1 < a) (_ : 1 < n), ¬ a ^ n ∣ a
+  | succ a, succ n, hp, hk, h =>
+    have : succ a * succ a ^ n ∣ succ a * 1 := by simpa [pow_succ'] using h
+    have : succ a ^ n ∣ 1 := Nat.dvd_of_mul_dvd_mul_left (succ_pos _) this
+    have he : succ a ^ n = 1 := eq_one_of_dvd_one this
+    have : n < succ a ^ n := lt_pow_self hp n
+    have : n < 1 := by rwa [he] at this
+    have : n = 0 := Nat.eq_zero_of_le_zero <| le_of_lt_succ this
+    have : 1 < 1 := by rwa [this] at hk
+    absurd this (by decide)
+#align nat.not_pos_pow_dvd Nat.not_pos_pow_dvd
+
+lemma lt_of_pow_dvd_right (hb : b ≠ 0) (ha : 2 ≤ a) (h : a ^ n ∣ b) : n < b := by
+  rw [← Nat.pow_lt_pow_iff_right (succ_le_iff.1 ha)]
+  exact lt_of_le_of_lt (le_of_dvd (Nat.pos_iff_ne_zero.2 hb) h) (lt_pow_self ha _)
+#align nat.lt_of_pow_dvd_right Nat.lt_of_pow_dvd_right
+
+lemma div_dvd_of_dvd (h : n ∣ m) : m / n ∣ m := ⟨n, (Nat.div_mul_cancel h).symm⟩
+#align nat.div_dvd_of_dvd Nat.div_dvd_of_dvd
+
+protected lemma div_div_self (h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n := by
+  rcases h with ⟨_, rfl⟩
+  rw [Nat.mul_ne_zero_iff] at hm
+  rw [mul_div_right _ (Nat.pos_of_ne_zero hm.1), mul_div_left _ (Nat.pos_of_ne_zero hm.2)]
+#align nat.div_div_self Nat.div_div_self
+
+lemma not_dvd_of_pos_of_lt (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n := by
+  rintro ⟨k, rfl⟩
+  rcases Nat.eq_zero_or_pos k with (rfl | hk)
+  · exact lt_irrefl 0 h1
+  · exact not_lt.2 (Nat.le_mul_of_pos_right _ hk) h2
+#align nat.not_dvd_of_pos_of_lt Nat.not_dvd_of_pos_of_lt
+
 lemma mod_eq_iff_lt (hn : n ≠ 0) : m % n = m ↔ m < n :=
   ⟨fun h ↦ by rw [← h]; exact mod_lt _ $ Nat.pos_iff_ne_zero.2 hn, mod_eq_of_lt⟩
 #align nat.mod_eq_iff_lt Nat.mod_eq_iff_lt
@@ -595,6 +1072,42 @@ protected lemma div_mod_unique (h : 0 < b) :
     rw [add_mul_div_left _ _ h, add_mul_mod_self_left]; simp [div_eq_of_lt, mod_eq_of_lt, h₂]⟩
 #align nat.div_mod_unique Nat.div_mod_unique
 
+/-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`. -/
+lemma sub_mod_eq_zero_of_mod_eq (h : m % k = n % k) : (m - n) % k = 0 := by
+  rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, ← Nat.sub_sub,
+    Nat.add_sub_cancel_left, ← Nat.mul_sub_left_distrib k, Nat.mul_mod_right]
+#align nat.sub_mod_eq_zero_of_mod_eq Nat.sub_mod_eq_zero_of_mod_eq
+
+@[simp] lemma one_mod (n : ℕ) : 1 % (n + 2) = 1 :=
+  Nat.mod_eq_of_lt (Nat.add_lt_add_right n.succ_pos 1)
+#align nat.one_mod Nat.one_mod
+
+lemma one_mod_of_ne_one : ∀ {n : ℕ}, n ≠ 1 → 1 % n = 1
+  | 0, _ | (n + 2), _ => by simp
+
+lemma dvd_sub_mod (k : ℕ) : n ∣ k - k % n :=
+  ⟨k / n, Nat.sub_eq_of_eq_add (Nat.div_add_mod k n).symm⟩
+#align nat.dvd_sub_mod Nat.dvd_sub_mod
+
+lemma add_mod_eq_ite :
+    (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k := by
+  cases k; simp only [zero_eq, mod_zero, zero_le, ↓reduceIte, Nat.sub_zero]
+  rw [Nat.add_mod]
+  split_ifs with h
+  · rw [Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]
+    exact (Nat.sub_lt_iff_lt_add h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _))
+      (n.mod_lt (zero_lt_succ _)))
+  · exact Nat.mod_eq_of_lt (lt_of_not_ge h)
+#align nat.add_mod_eq_ite Nat.add_mod_eq_ite
+
+/-- `m` is not divisible by `n` if it is between `n * k` and `n * (k + 1)` for some `k`. -/
+theorem not_dvd_of_between_consec_multiples (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m := by
+  rintro ⟨d, rfl⟩
+  have := Nat.lt_of_mul_lt_mul_left h1
+  have := Nat.lt_of_mul_lt_mul_left h2
+  omega
+#align nat.not_dvd_of_between_consec_multiples Nat.not_dvd_of_between_consec_multiples
+
 -- TODO: Replace `Nat.dvd_add_iff_left`
 protected lemma dvd_add_left (h : a ∣ c) : a ∣ b + c ↔ a ∣ b := (Nat.dvd_add_iff_left h).symm
 #align nat.dvd_add_left Nat.dvd_add_left
@@ -643,11 +1156,6 @@ lemma eq_zero_of_dvd_of_div_eq_zero (hab : a ∣ b) (h : b / a = 0) : b = 0 := b
   rw [← Nat.div_mul_cancel hab, h, Nat.zero_mul]
 #align nat.eq_zero_of_dvd_of_div_eq_zero Nat.eq_zero_of_dvd_of_div_eq_zero
 
-@[gcongr]
-lemma div_le_div_left (hcb : c ≤ b) (hc : 0 < c) : a / b ≤ a / c :=
-  (Nat.le_div_iff_mul_le hc).2 <| le_trans (Nat.mul_le_mul_left _ hcb) (div_mul_le_self _ _)
-#align nat.div_le_div_left Nat.div_le_div_left
-
 @[gcongr]
 protected theorem div_le_div {a b c d : ℕ} (h1 : a ≤ b) (h2 : d ≤ c) (h3 : d ≠ 0) : a / c ≤ b / d :=
   calc a / c ≤ b / c := Nat.div_le_div_right h1
@@ -717,6 +1225,23 @@ lemma find_comp_succ (h₁ : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h0 : ¬ p 0)
   exacts [h0, @Nat.find_min (fun n ↦ p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)]
 #align nat.find_comp_succ Nat.find_comp_succ
 
+-- Porting note (#10618): removing `simp` attribute as `simp` can prove it
+lemma find_pos (h : ∃ n : ℕ, p n) : 0 < Nat.find h ↔ ¬p 0 :=
+  Nat.pos_iff_ne_zero.trans (Nat.find_eq_zero _).not
+#align nat.find_pos Nat.find_pos
+
+lemma find_add {hₘ : ∃ m, p (m + n)} {hₙ : ∃ n, p n} (hn : n ≤ Nat.find hₙ) :
+    Nat.find hₘ + n = Nat.find hₙ := by
+  refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_
+  · have hnm : n ≤ m := le_trans hn (find_le hpm)
+    refine Nat.add_le_of_le_sub hnm (find_le ?_)
+    rwa [Nat.sub_add_cancel hnm]
+  · rw [← Nat.sub_le_iff_le_add]
+    refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_
+    rw [Nat.sub_le_iff_le_add]
+    exact find_le hpm
+#align nat.find_add Nat.find_add
+
 end Find
 
 /-! ### `Nat.findGreatest` -/
@@ -749,6 +1274,90 @@ lemma findGreatest_of_not (h : ¬ P (n + 1)) : findGreatest P (n + 1) = findGrea
   simp [Nat.findGreatest, h]
 #align nat.find_greatest_of_not Nat.findGreatest_of_not
 
+lemma findGreatest_eq_iff :
+    Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n⦄, m < n → n ≤ k → ¬P n := by
+  induction' k with k ihk generalizing m
+  · rw [eq_comm, Iff.comm]
+    simp only [zero_eq, Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
+    rintro rfl
+    exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by omega⟩
+  · by_cases hk : P (k + 1)
+    · rw [findGreatest_eq hk]
+      constructor
+      · rintro rfl
+        exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by omega⟩
+      · rintro ⟨hle, h0, hm⟩
+        rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt)
+        exacts [rfl, (hm hlt (le_refl _) hk).elim]
+    · rw [findGreatest_of_not hk, ihk]
+      constructor
+      · rintro ⟨hle, hP, hm⟩
+        refine ⟨le_trans hle k.le_succ, hP, fun n hlt hle ↦ ?_⟩
+        rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt')
+        exacts [hk, hm hlt <| Nat.lt_succ_iff.1 hlt']
+      · rintro ⟨hle, hP, hm⟩
+        refine ⟨Nat.lt_succ_iff.1 (lt_of_le_of_ne hle ?_), hP,
+          fun n hlt hle ↦ hm hlt (le_trans hle k.le_succ)⟩
+        rintro rfl
+        exact hk (hP k.succ_ne_zero)
+#align nat.find_greatest_eq_iff Nat.findGreatest_eq_iff
+
+lemma findGreatest_eq_zero_iff : Nat.findGreatest P k = 0 ↔ ∀ ⦃n⦄, 0 < n → n ≤ k → ¬P n := by
+  simp [findGreatest_eq_iff]
+#align nat.find_greatest_eq_zero_iff Nat.findGreatest_eq_zero_iff
+
+@[simp] lemma findGreatest_pos : 0 < Nat.findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n := by
+  rw [Nat.pos_iff_ne_zero, Ne.def, findGreatest_eq_zero_iff]; push_neg; rfl
+
+lemma findGreatest_spec (hmb : m ≤ n) (hm : P m) : P (Nat.findGreatest P n) := by
+  by_cases h : Nat.findGreatest P n = 0
+  · cases m
+    · rwa [h]
+    exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim
+  · exact (findGreatest_eq_iff.1 rfl).2.1 h
+#align nat.find_greatest_spec Nat.findGreatest_spec
+
+lemma findGreatest_le (n : ℕ) : Nat.findGreatest P n ≤ n :=
+  (findGreatest_eq_iff.1 rfl).1
+#align nat.find_greatest_le Nat.findGreatest_le
+
+lemma le_findGreatest (hmb : m ≤ n) (hm : P m) : m ≤ Nat.findGreatest P n :=
+  le_of_not_lt fun hlt => (findGreatest_eq_iff.1 rfl).2.2 hlt hmb hm
+#align nat.le_find_greatest Nat.le_findGreatest
+
+lemma findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] {m n} (hmn : m ≤ n) :
+    Nat.findGreatest P m ≤ Nat.findGreatest P n := by
+  induction' hmn with k hmk ih
+  · simp
+  rw [findGreatest_succ]
+  split_ifs
+  · exact le_trans ih $ le_trans (findGreatest_le _) (le_succ _)
+  · exact ih
+#align nat.find_greatest_mono_right Nat.findGreatest_mono_right
+
+lemma findGreatest_mono_left [DecidablePred Q] (hPQ : ∀ n, P n → Q n) (n : ℕ) :
+    Nat.findGreatest P n ≤ Nat.findGreatest Q n := by
+  induction' n with n hn
+  · rfl
+  by_cases h : P (n + 1)
+  · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
+  · rw [findGreatest_of_not h]
+    exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)
+#align nat.find_greatest_mono_left Nat.findGreatest_mono_left
+
+lemma findGreatest_mono [DecidablePred Q] (hPQ : ∀ n, P n → Q n) (hmn : m ≤ n) :
+    Nat.findGreatest P m ≤ Nat.findGreatest Q n :=
+  le_trans (Nat.findGreatest_mono_right _ hmn) (findGreatest_mono_left hPQ _)
+#align nat.find_greatest_mono Nat.findGreatest_mono
+
+theorem findGreatest_is_greatest (hk : Nat.findGreatest P n < k) (hkb : k ≤ n) : ¬P k :=
+  (findGreatest_eq_iff.1 rfl).2.2 hk hkb
+#align nat.find_greatest_is_greatest Nat.findGreatest_is_greatest
+
+theorem findGreatest_of_ne_zero (h : Nat.findGreatest P n = m) (h0 : m ≠ 0) : P m :=
+  (findGreatest_eq_iff.1 h).2.1 h0
+#align nat.find_greatest_of_ne_zero Nat.findGreatest_of_ne_zero
+
 end FindGreatest
 
 /-! ### Decidability of predicates -/
@@ -759,4 +1368,19 @@ end FindGreatest
 #align nat.decidable_exists_lt Nat.decidableExistsLT
 #align nat.decidable_exists_le Nat.decidableExistsLE
 
+instance decidableLoHi (lo hi : ℕ) (P : ℕ → Prop) [H : DecidablePred P] :
+    Decidable (∀ x, lo ≤ x → x < hi → P x) :=
+  decidable_of_iff (∀ x < hi - lo, P (lo + x)) $ by
+    refine ⟨fun al x hl hh ↦ ?_,
+      fun al x h ↦ al _ (Nat.le_add_right _ _) (Nat.lt_sub_iff_add_lt'.1 h)⟩
+    have := al (x - lo) ((Nat.sub_lt_sub_iff_right hl).2 hh)
+    rwa [Nat.add_sub_cancel' hl] at this
+#align nat.decidable_lo_hi Nat.decidableLoHi
+
+instance decidableLoHiLe (lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] :
+    Decidable (∀ x, lo ≤ x → x ≤ hi → P x) :=
+  decidable_of_iff (∀ x, lo ≤ x → x < hi + 1 → P x) <|
+    ball_congr fun _ _ => imp_congr Nat.lt_succ_iff Iff.rfl
+#align nat.decidable_lo_hi_le Nat.decidableLoHiLe
+
 end Nat
diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index e4b4eb1bcd1c6..3348b1855bca7 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -3,9 +3,12 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Chris Hughes, Floris van Doorn, Yaël Dillies
 -/
+import Mathlib.Algebra.Divisibility.Basic
+import Mathlib.Data.Nat.Basic
+import Mathlib.Order.Monotone.Basic
 import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.Common
-import Mathlib.Algebra.GroupPower.Order
+import Mathlib.Tactic.Monotonicity.Attr
 
 #align_import data.nat.factorial.basic from "leanprover-community/mathlib"@"d012cd09a9b256d870751284dd6a29882b0be105"
 
@@ -57,12 +60,12 @@ theorem factorial_succ (n : ℕ) : (n + 1)! = (n + 1) * n ! :=
 #align nat.factorial_two Nat.factorial_two
 
 theorem mul_factorial_pred (hn : 0 < n) : n * (n - 1)! = n ! :=
-  tsub_add_cancel_of_le (Nat.succ_le_of_lt hn) ▸ rfl
+  Nat.sub_add_cancel (Nat.succ_le_of_lt hn) ▸ rfl
 #align nat.mul_factorial_pred Nat.mul_factorial_pred
 
 theorem factorial_pos : ∀ n, 0 < n !
-  | 0 => zero_lt_one
-  | succ n => mul_pos (succ_pos _) (factorial_pos n)
+  | 0 => Nat.zero_lt_one
+  | succ n => Nat.mul_pos (succ_pos _) (factorial_pos n)
 #align nat.factorial_pos Nat.factorial_pos
 
 theorem factorial_ne_zero (n : ℕ) : n ! ≠ 0 :=
@@ -100,8 +103,8 @@ theorem factorial_lt (hn : 0 < n) : n ! < m ! ↔ n < m := by
   refine' ⟨fun h => not_le.mp fun hmn => not_le_of_lt h (factorial_le hmn), fun h => _⟩
   have : ∀ {n}, 0 < n → n ! < (n + 1)! := by
     intro k hk
-    rw [factorial_succ, succ_mul, lt_add_iff_pos_left]
-    exact mul_pos hk k.factorial_pos
+    rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
+    exact Nat.mul_pos hk k.factorial_pos
   induction' h with k hnk ih generalizing hn
   · exact this hn
   · exact (ih hn).trans (this <| hn.trans <| lt_of_succ_le hnk)
@@ -110,9 +113,7 @@ theorem factorial_lt (hn : 0 < n) : n ! < m ! ↔ n < m := by
 @[gcongr]
 lemma factorial_lt_of_lt {m n : ℕ} (hn : 0 < n) (h : n < m) : n ! < m ! := (factorial_lt hn).mpr h
 
-@[simp]
-theorem one_lt_factorial : 1 < n ! ↔ 1 < n :=
-  factorial_lt one_pos
+@[simp] lemma one_lt_factorial : 1 < n ! ↔ 1 < n := factorial_lt Nat.one_pos
 #align nat.one_lt_factorial Nat.one_lt_factorial
 
 @[simp]
@@ -127,11 +128,11 @@ theorem factorial_eq_one : n ! = 1 ↔ n ≤ 1 := by
 theorem factorial_inj (hn : 1 < n) : n ! = m ! ↔ n = m := by
   refine' ⟨fun h => _, congr_arg _⟩
   obtain hnm | rfl | hnm := lt_trichotomy n m
-  · rw [← factorial_lt <| pos_of_gt hn, h] at hnm
+  · rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
     cases lt_irrefl _ hnm
   · rfl
   rw [← one_lt_factorial, h, one_lt_factorial] at hn
-  rw [← factorial_lt <| pos_of_gt hn, h] at hnm
+  rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
   cases lt_irrefl _ hnm
 #align nat.factorial_inj Nat.factorial_inj
 
@@ -141,33 +142,30 @@ theorem factorial_inj' (h : 1 < n ∨ 1 < m) : n ! = m ! ↔ n = m := by
   · rw [eq_comm, factorial_inj hm, eq_comm]
 
 theorem self_le_factorial : ∀ n : ℕ, n ≤ n !
-  | 0 => zero_le_one
-  | k + 1 => le_mul_of_one_le_right k.zero_lt_succ.le (Nat.one_le_of_lt <| Nat.factorial_pos _)
+  | 0 => Nat.zero_le _
+  | k + 1 => Nat.le_mul_of_pos_right _ (Nat.one_le_of_lt k.factorial_pos)
 #align nat.self_le_factorial Nat.self_le_factorial
 
 theorem lt_factorial_self {n : ℕ} (hi : 3 ≤ n) : n < n ! := by
-  have : 0 < n := (zero_lt_two (α := ℕ)).trans (succ_le_iff.mp hi)
-  have : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
+  have : 0 < n := Nat.zero_lt_two.trans (succ_le_iff.mp hi)
+  have hn : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
   rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]
-  exact
-    lt_mul_of_one_lt_right (pred n).succ_pos
-      ((‹1 < pred n›).trans_le (self_le_factorial _))
+  exact (Nat.lt_mul_iff_one_lt_right (pred n).succ_pos).2 (hn.trans_le (self_le_factorial _))
 #align nat.lt_factorial_self Nat.lt_factorial_self
 
 theorem add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :
     i + (n + 1)! < (i + n + 1)! := by
   rw [factorial_succ (i + _), add_mul, one_mul]
   have : i ≤ i + n := le.intro rfl
-  exact
-    add_lt_add_of_lt_of_le
+  exact Nat.add_lt_add_of_lt_of_le
       (this.trans_lt
-        ((lt_mul_iff_one_lt_right ((by decide : 0 < 2).trans_le (hi.trans this))).mpr
+        ((Nat.lt_mul_iff_one_lt_right ((by decide : 0 < 2).trans_le (hi.trans this))).mpr
           (lt_iff_le_and_ne.mpr
             ⟨(i + n).factorial_pos, fun g =>
               Nat.not_succ_le_self 1 ((hi.trans this).trans (factorial_eq_one.mp g.symm))⟩)))
       (factorial_le
         ((le_of_eq (add_comm n 1)).trans
-        ((add_le_add_iff_right n).mpr ((by decide : 1 ≤ 2).trans hi))))
+        (Nat.add_le_add_iff_right.2 ((by decide : 1 ≤ 2).trans hi))))
 #align nat.add_factorial_succ_lt_factorial_add_succ Nat.add_factorial_succ_lt_factorial_add_succ
 
 theorem add_factorial_lt_factorial_add {i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) :
@@ -188,10 +186,9 @@ theorem add_factorial_succ_le_factorial_add_succ (i : ℕ) (n : ℕ) :
   · match i with
     | 0 => simp
     | 1 =>
-      rw [← add_assoc, factorial_succ (1 + n), add_mul, one_mul, add_comm 1 n, add_le_add_iff_right]
-      apply one_le_mul
-      · apply Nat.le_add_left
-      · apply factorial_pos
+      rw [← add_assoc, factorial_succ (1 + n), add_mul, one_mul, add_comm 1 n,
+        Nat.add_le_add_iff_right]
+      exact Nat.mul_pos n.succ_pos n.succ.factorial_pos
     | succ (succ n) => contradiction
 #align nat.add_factorial_succ_le_factorial_add_succ Nat.add_factorial_succ_le_factorial_add_succ
 
@@ -203,7 +200,7 @@ theorem add_factorial_le_factorial_add (i : ℕ) {n : ℕ} (n1 : 1 ≤ n) : i +
 
 theorem factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) : n ! * n ^ (m - n) ≤ m ! := by
   calc
-    _ ≤ n ! * (n + 1) ^ (m - n) := mul_le_mul_left' (Nat.pow_le_pow_left n.le_succ _) _
+    _ ≤ n ! * (n + 1) ^ (m - n) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
     _ ≤ _ := by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)
 #align nat.factorial_mul_pow_sub_le_factorial Nat.factorial_mul_pow_sub_le_factorial
 
@@ -211,8 +208,8 @@ lemma factorial_le_pow : ∀ n, n ! ≤ n ^ n
   | 0 => le_rfl
   | n + 1 =>
     calc
-      _ ≤ (n + 1) * n ^ n := mul_le_mul_left' n.factorial_le_pow _
-      _ ≤ (n + 1) * (n + 1) ^ n := mul_le_mul_left' (Nat.pow_le_pow_left n.le_succ _) _
+      _ ≤ (n + 1) * n ^ n := Nat.mul_le_mul_left _ n.factorial_le_pow
+      _ ≤ (n + 1) * (n + 1) ^ n := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
       _ = _ := by rw [pow_succ']
 
 end Factorial
@@ -306,8 +303,8 @@ theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, n ^ k ≤ n.ascFactori
 
 theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2) := by
   rw [Nat.pow_succ, ascFactorial, mul_comm]
-  exact Nat.mul_lt_mul_of_lt_of_le' (lt_add_of_pos_right (n + 1) (succ_pos k))
-    (pow_succ_le_ascFactorial n.succ _) (NeZero.pos ((n + 1) ^ (k + 1)))
+  exact Nat.mul_lt_mul_of_lt_of_le' (Nat.lt_add_of_pos_right k.succ_pos)
+    (pow_succ_le_ascFactorial n.succ _) (Nat.pow_pos n.succ_pos)
 #align nat.pow_lt_asc_factorial' Nat.pow_lt_ascFactorial'
 
 theorem pow_lt_ascFactorial (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k
@@ -330,11 +327,11 @@ theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1).a
   | k + 2 => fun _ => by
     rw [Nat.pow_succ, mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]
     exact Nat.mul_lt_mul_of_le_of_lt le_rfl ((ascFactorial_le_pow_add n _).trans_lt
-      (pow_lt_pow_left (@lt_add_one ℕ _ _ _ _ _ _ _) (zero_le _) k.succ_ne_zero)) (succ_pos _)
+      (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero)) (succ_pos _)
 #align nat.asc_factorial_lt_pow_add Nat.ascFactorial_lt_pow_add
 
 theorem ascFactorial_pos (n k : ℕ) : 0 < (n + 1).ascFactorial k :=
-  (pow_pos (succ_pos n) k).trans_le (pow_succ_le_ascFactorial (n + 1) k)
+  (Nat.pow_pos n.succ_pos).trans_le (pow_succ_le_ascFactorial (n + 1) k)
 #align nat.asc_factorial_pos Nat.ascFactorial_pos
 
 end AscFactorial
@@ -360,7 +357,7 @@ theorem descFactorial_succ (n k : ℕ) : n.descFactorial (k + 1) = (n - k) * n.d
 #align nat.desc_factorial_succ Nat.descFactorial_succ
 
 theorem zero_descFactorial_succ (k : ℕ) : (0 : ℕ).descFactorial (k + 1) = 0 := by
-  rw [descFactorial_succ, zero_tsub, zero_mul]
+  rw [descFactorial_succ, Nat.zero_sub, zero_mul]
 #align nat.zero_desc_factorial_succ Nat.zero_descFactorial_succ
 
 theorem descFactorial_one (n : ℕ) : n.descFactorial 1 = n := by simp
@@ -376,7 +373,7 @@ theorem succ_descFactorial_succ (n : ℕ) :
 
 theorem succ_descFactorial (n : ℕ) :
     ∀ k, (n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k
-  | 0 => by rw [tsub_zero, descFactorial_zero, descFactorial_zero]
+  | 0 => by rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]
   | k + 1 => by
     rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, mul_left_comm]
 #align nat.succ_desc_factorial Nat.succ_descFactorial
@@ -391,7 +388,7 @@ theorem descFactorial_eq_zero_iff_lt {n : ℕ} : ∀ {k : ℕ}, n.descFactorial
   | 0 => by simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]
   | succ k => by
     rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
-      tsub_eq_zero_iff_le, lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
+      Nat.sub_eq_zero_iff_le, lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
     exact fun h _ => h
 #align nat.desc_factorial_eq_zero_iff_lt Nat.descFactorial_eq_zero_iff_lt
 
@@ -417,7 +414,7 @@ theorem add_descFactorial_eq_ascFactorial' (n : ℕ) :
 /-- `n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div`
 for the version using ℕ-division. -/
 theorem factorial_mul_descFactorial : ∀ {n k : ℕ}, k ≤ n → (n - k)! * n.descFactorial k = n !
-  | n, 0 => fun _ => by rw [descFactorial_zero, mul_one, tsub_zero]
+  | n, 0 => fun _ => by rw [descFactorial_zero, mul_one, Nat.sub_zero]
   | 0, succ k => fun h => by
     exfalso
     exact not_succ_le_zero k h
@@ -438,7 +435,7 @@ theorem pow_sub_le_descFactorial (n : ℕ) : ∀ k : ℕ, (n + 1 - k) ^ k ≤ n.
   | k + 1 => by
     rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, mul_comm]
     apply Nat.mul_le_mul_left
-    exact (le_trans (Nat.pow_le_pow_left (tsub_le_tsub_right (le_succ _) _) k)
+    exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
       (pow_sub_le_descFactorial n k))
 #align nat.pow_sub_le_desc_factorial Nat.pow_sub_le_descFactorial
 
@@ -446,16 +443,14 @@ theorem pow_sub_lt_descFactorial' {n : ℕ} :
     ∀ {k : ℕ}, k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
   | 0 => fun h => by
     rw [descFactorial_succ, pow_succ, pow_one, descFactorial_one]
-    exact
-      Nat.mul_lt_mul_of_pos_left (tsub_lt_self (lt_of_lt_of_le zero_lt_two h) zero_lt_one)
-        (tsub_pos_of_lt h)
+    exact Nat.mul_lt_mul_of_pos_left (Nat.sub_lt_self Nat.zero_lt_one (Nat.zero_lt_two.trans_le h))
+      (Nat.sub_pos_of_lt h)
   | k + 1 => fun h => by
     rw [descFactorial_succ, Nat.pow_succ, mul_comm]
-    apply Nat.mul_lt_mul_of_pos_left
-    · refine' ((Nat.pow_le_pow_left (tsub_le_tsub_right (le_succ n) _) _).trans_lt _)
-      rw [succ_sub_succ]
-      exact pow_sub_lt_descFactorial' ((le_succ _).trans h)
-    · apply tsub_pos_of_lt; apply h
+    refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)
+    refine (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _).trans_lt ?_
+    rw [succ_sub_succ]
+    exact pow_sub_lt_descFactorial' ((le_succ _).trans h)
 #align nat.pow_sub_lt_desc_factorial' Nat.pow_sub_lt_descFactorial'
 
 theorem pow_sub_lt_descFactorial {n : ℕ} :
@@ -479,22 +474,23 @@ theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k 
   | 1 => by intro; contradiction
   | k + 2 => fun _ => by
     rw [descFactorial_succ, pow_succ', mul_comm, mul_comm n]
-    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ)
-      (pow_pos (Nat.lt_of_succ_le hn) _)
+    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (Nat.sub_lt hn k.zero_lt_succ)
+      (Nat.pow_pos (Nat.lt_of_succ_le hn))
 #align nat.desc_factorial_lt_pow Nat.descFactorial_lt_pow
 
 end DescFactorial
 
 lemma factorial_two_mul_le (n : ℕ) : (2 * n)! ≤ (2 * n) ^ n * n ! := by
   rw [two_mul, ← factorial_mul_ascFactorial, mul_comm]
-  exact mul_le_mul_right' (ascFactorial_le_pow_add _ _) _
+  exact Nat.mul_le_mul_right _ (ascFactorial_le_pow_add _ _)
 
 lemma two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n ! ≤ (2 * n) ! := by
   obtain _ | n := n
   · simp
   rw [mul_comm, two_mul]
   calc
-    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) := mul_le_mul_left' (pow_le_pow_of_le_left le_add_self _) _
+    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) :=
+      Nat.mul_le_mul_left _ (pow_le_pow_of_le_left (le_add_left _ _) _)
     _ ≤ _ := Nat.factorial_mul_pow_le_factorial
 
 end Nat
diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean
index cd182fb2d4769..017f82d19bf7a 100644
--- a/Mathlib/Data/Nat/Log.lean
+++ b/Mathlib/Data/Nat/Log.lean
@@ -3,8 +3,9 @@ Copyright (c) 2020 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yaël Dillies
 -/
-import Mathlib.Data.Nat.Pow
+import Mathlib.Data.Nat.Defs
 import Mathlib.Data.Set.Intervals.Basic
+import Mathlib.Tactic.Monotonicity.Attr
 
 #align_import data.nat.log from "leanprover-community/mathlib"@"3e00d81bdcbf77c8188bbd18f5524ddc3ed8cac6"
 
@@ -31,7 +32,7 @@ such that `b^k ≤ n`, so if `b^k = n`, it returns exactly `k`. -/
 def log (b : ℕ) : ℕ → ℕ
   | n =>
     if h : b ≤ n ∧ 1 < b then
-      have : n / b < n := div_lt_self ((zero_lt_one.trans h.2).trans_le h.1) h.2
+      have : n / b < n := div_lt_self ((Nat.zero_lt_one.trans h.2).trans_le h.1) h.2
       log b (n / b) + 1
     else 0
 #align nat.log Nat.log
@@ -52,7 +53,7 @@ theorem log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n) : log b n = 0 :=
 
 @[simp]
 theorem log_pos_iff {b n : ℕ} : 0 < log b n ↔ b ≤ n ∧ 1 < b := by
-  rw [pos_iff_ne_zero, Ne.def, log_eq_zero_iff, not_or, not_lt, not_le]
+  rw [Nat.pos_iff_ne_zero, Ne.def, log_eq_zero_iff, not_or, not_lt, not_le]
 #align nat.log_pos_iff Nat.log_pos_iff
 
 theorem log_pos {b n : ℕ} (hb : 1 < b) (hbn : b ≤ n) : 0 < log b n :=
@@ -64,9 +65,7 @@ theorem log_of_one_lt_of_le {b n : ℕ} (h : 1 < b) (hn : b ≤ n) : log b n = l
   exact if_pos ⟨hn, h⟩
 #align nat.log_of_one_lt_of_le Nat.log_of_one_lt_of_le
 
-@[simp]
-theorem log_zero_left : ∀ n, log 0 n = 0 :=
-  log_of_left_le_one zero_le_one
+@[simp] lemma log_zero_left : ∀ n, log 0 n = 0 := log_of_left_le_one $ Nat.zero_le _
 #align nat.log_zero_left Nat.log_zero_left
 
 @[simp]
@@ -90,13 +89,13 @@ theorem pow_le_iff_le_log {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : y ≠ 0) :
     b ^ x ≤ y ↔ x ≤ log b y := by
   induction' y using Nat.strong_induction_on with y ih generalizing x
   cases x with
-  | zero => exact iff_of_true hy.bot_lt (zero_le _)
+  | zero => dsimp; omega
   | succ x =>
     rw [log]; split_ifs with h
-    · have b_pos : 0 < b := zero_le_one.trans_lt hb
-      rw [succ_eq_add_one, add_le_add_iff_right, ←
-        ih (y / b) (div_lt_self hy.bot_lt hb) (Nat.div_pos h.1 b_pos).ne', le_div_iff_mul_le b_pos,
-        pow_succ', mul_comm]
+    · have b_pos : 0 < b := lt_of_succ_lt hb
+      rw [succ_eq_add_one, Nat.add_le_add_iff_right, ← ih (y / b) (div_lt_self
+        (Nat.pos_iff_ne_zero.2 hy) hb) (Nat.div_pos h.1 b_pos).ne', le_div_iff_mul_le b_pos,
+        pow_succ', Nat.mul_comm]
     · exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩)
         (not_succ_le_zero _)
 #align nat.pow_le_iff_le_log Nat.pow_le_iff_le_log
@@ -107,13 +106,13 @@ theorem lt_pow_iff_log_lt {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : y ≠ 0) : y
 
 theorem pow_le_of_le_log {b x y : ℕ} (hy : y ≠ 0) (h : x ≤ log b y) : b ^ x ≤ y := by
   refine' (le_or_lt b 1).elim (fun hb => _) fun hb => (pow_le_iff_le_log hb hy).2 h
-  rw [log_of_left_le_one hb, nonpos_iff_eq_zero] at h
-  rwa [h, pow_zero, one_le_iff_ne_zero]
+  rw [log_of_left_le_one hb, Nat.le_zero] at h
+  rwa [h, Nat.pow_zero, one_le_iff_ne_zero]
 #align nat.pow_le_of_le_log Nat.pow_le_of_le_log
 
 theorem le_log_of_pow_le {b x y : ℕ} (hb : 1 < b) (h : b ^ x ≤ y) : x ≤ log b y := by
   rcases ne_or_eq y 0 with (hy | rfl)
-  exacts [(pow_le_iff_le_log hb hy).1 h, (h.not_lt (pow_pos (zero_lt_one.trans hb) _)).elim]
+  exacts [(pow_le_iff_le_log hb hy).1 h, (h.not_lt (Nat.pow_pos (Nat.zero_lt_one.trans hb))).elim]
 #align nat.le_log_of_pow_le Nat.le_log_of_pow_le
 
 theorem pow_log_le_self (b : ℕ) {x : ℕ} (hx : x ≠ 0) : b ^ log b x ≤ x :=
@@ -137,28 +136,31 @@ theorem log_eq_iff {b m n : ℕ} (h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0) :
   rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
   · rw [le_antisymm_iff, ← Nat.lt_succ_iff, ← pow_le_iff_le_log, ← lt_pow_iff_log_lt, and_comm] <;>
       assumption
-  · have hm : m ≠ 0 := h.resolve_right hbn
-    rw [not_and_or, not_lt, Ne.def, not_not] at hbn
-    rcases hbn with (hb | rfl)
-    · simpa only [log_of_left_le_one hb, hm.symm, false_iff_iff, not_and, not_lt] using
-        le_trans (pow_le_pow_right_of_le_one' hb m.le_succ)
-    · simp [@eq_comm _ 0, hm]
+  have hm : m ≠ 0 := h.resolve_right hbn
+  rw [not_and_or, not_lt, Ne.def, not_not] at hbn
+  rcases hbn with (hb | rfl)
+  · obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb
+    any_goals
+      simp only [ne_eq, zero_eq, reduceSucc, lt_self_iff_false,  not_lt_zero, false_and, or_false]
+        at h
+      simp [h, eq_comm (a := 0), Nat.zero_pow (Nat.pos_iff_ne_zero.2 _)] <;> omega
+  · simp [@eq_comm _ 0, hm]
 #align nat.log_eq_iff Nat.log_eq_iff
 
 theorem log_eq_of_pow_le_of_lt_pow {b m n : ℕ} (h₁ : b ^ m ≤ n) (h₂ : n < b ^ (m + 1)) :
     log b n = m := by
   rcases eq_or_ne m 0 with (rfl | hm)
-  · rw [pow_one] at h₂
+  · rw [Nat.pow_one] at h₂
     exact log_of_lt h₂
   · exact (log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩
 #align nat.log_eq_of_pow_le_of_lt_pow Nat.log_eq_of_pow_le_of_lt_pow
 
 theorem log_pow {b : ℕ} (hb : 1 < b) (x : ℕ) : log b (b ^ x) = x :=
-  log_eq_of_pow_le_of_lt_pow le_rfl (pow_lt_pow_right hb x.lt_succ_self)
+  log_eq_of_pow_le_of_lt_pow le_rfl (Nat.pow_lt_pow_right hb x.lt_succ_self)
 #align nat.log_pow Nat.log_pow
 
 theorem log_eq_one_iff' {b n : ℕ} : log b n = 1 ↔ b ≤ n ∧ n < b * b := by
-  rw [log_eq_iff (Or.inl one_ne_zero), pow_add, pow_one]
+  rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]
 #align nat.log_eq_one_iff' Nat.log_eq_one_iff'
 
 theorem log_eq_one_iff {b n : ℕ} : log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n :=
@@ -167,9 +169,9 @@ theorem log_eq_one_iff {b n : ℕ} : log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b 
 #align nat.log_eq_one_iff Nat.log_eq_one_iff
 
 theorem log_mul_base {b n : ℕ} (hb : 1 < b) (hn : n ≠ 0) : log b (n * b) = log b n + 1 := by
-  apply log_eq_of_pow_le_of_lt_pow <;> rw [pow_succ', mul_comm b]
-  exacts [mul_le_mul_right' (pow_log_le_self _ hn) _,
-    (mul_lt_mul_right (zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]
+  apply log_eq_of_pow_le_of_lt_pow <;> rw [pow_succ', Nat.mul_comm b]
+  exacts [Nat.mul_le_mul_right _ (pow_log_le_self _ hn),
+    (Nat.mul_lt_mul_right (Nat.zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]
 #align nat.log_mul_base Nat.log_mul_base
 
 theorem pow_log_le_add_one (b : ℕ) : ∀ x, b ^ log b x ≤ x + 1
@@ -195,7 +197,7 @@ theorem log_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ lo
   rcases eq_or_ne n 0 with (rfl | hn); · rw [log_zero_right, log_zero_right]
   apply le_log_of_pow_le hc
   calc
-    c ^ log b n ≤ b ^ log b n := pow_le_pow_left' hb _
+    c ^ log b n ≤ b ^ log b n := Nat.pow_le_pow_left hb _
     _ ≤ n := pow_log_le_self _ hn
 #align nat.log_anti_left Nat.log_anti_left
 
@@ -209,7 +211,7 @@ theorem log_div_base (b n : ℕ) : log b (n / b) = log b n - 1 := by
   · rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
   cases' lt_or_le n b with h h
   · rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
-  rw [log_of_one_lt_of_le hb h, add_tsub_cancel_right]
+  rw [log_of_one_lt_of_le hb h, Nat.add_sub_cancel_right]
 #align nat.log_div_base Nat.log_div_base
 
 @[simp]
@@ -217,15 +219,15 @@ theorem log_div_mul_self (b n : ℕ) : log b (n / b * b) = log b n := by
   rcases le_or_lt b 1 with hb | hb
   · rw [log_of_left_le_one hb, log_of_left_le_one hb]
   cases' lt_or_le n b with h h
-  · rw [div_eq_of_lt h, zero_mul, log_zero_right, log_of_lt h]
-  rw [log_mul_base hb (Nat.div_pos h (zero_le_one.trans_lt hb)).ne', log_div_base,
-    tsub_add_cancel_of_le (succ_le_iff.2 <| log_pos hb h)]
+  · rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]
+  rw [log_mul_base hb (Nat.div_pos h (by omega)).ne', log_div_base,
+    Nat.sub_add_cancel (succ_le_iff.2 <| log_pos hb h)]
 #align nat.log_div_mul_self Nat.log_div_mul_self
 
 theorem add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) / b < n := by
-  rw [div_lt_iff_lt_mul (zero_lt_one.trans hb), ← succ_le_iff, ← pred_eq_sub_one,
-    succ_pred_eq_of_pos (add_pos (zero_lt_one.trans hn) (zero_lt_one.trans hb))]
-  exact add_le_mul hn hb
+  rw [div_lt_iff_lt_mul (by omega), ← succ_le_iff, ← pred_eq_sub_one,
+    succ_pred_eq_of_pos (by omega)]
+  exact Nat.add_le_mul hn hb
 -- Porting note: Was private in mathlib 3
 -- #align nat.add_pred_div_lt Nat.add_pred_div_lt
 
@@ -251,14 +253,10 @@ theorem clog_of_right_le_one {n : ℕ} (hn : n ≤ 1) (b : ℕ) : clog b n = 0 :
   rw [clog, dif_neg fun h : 1 < b ∧ 1 < n => h.2.not_le hn]
 #align nat.clog_of_right_le_one Nat.clog_of_right_le_one
 
-@[simp]
-theorem clog_zero_left (n : ℕ) : clog 0 n = 0 :=
-  clog_of_left_le_one zero_le_one _
+@[simp] lemma clog_zero_left (n : ℕ) : clog 0 n = 0 := clog_of_left_le_one (Nat.zero_le _) _
 #align nat.clog_zero_left Nat.clog_zero_left
 
-@[simp]
-theorem clog_zero_right (b : ℕ) : clog b 0 = 0 :=
-  clog_of_right_le_one zero_le_one _
+@[simp] lemma clog_zero_right (b : ℕ) : clog b 0 = 0 := clog_of_right_le_one (Nat.zero_le _) _
 #align nat.clog_zero_right Nat.clog_zero_right
 
 @[simp]
@@ -282,27 +280,24 @@ theorem clog_pos {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : 0 < clog b n := by
 
 theorem clog_eq_one {b n : ℕ} (hn : 2 ≤ n) (h : n ≤ b) : clog b n = 1 := by
   rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]
-  have n_pos : 0 < n := (zero_lt_two' ℕ).trans_le hn
-  rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul (n_pos.trans_le h), ← succ_le_iff, ← pred_eq_sub_one,
-    succ_pred_eq_of_pos (add_pos n_pos (n_pos.trans_le h)), succ_mul, one_mul]
-  exact add_le_add_right h _
+  rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul] <;> omega
 #align nat.clog_eq_one Nat.clog_eq_one
 
 /-- `clog b` and `pow b` form a Galois connection. -/
 theorem le_pow_iff_clog_le {b : ℕ} (hb : 1 < b) {x y : ℕ} : x ≤ b ^ y ↔ clog b x ≤ y := by
   induction' x using Nat.strong_induction_on with x ih generalizing y
   cases y
-  · rw [pow_zero]
+  · rw [Nat.pow_zero]
     refine' ⟨fun h => (clog_of_right_le_one h b).le, _⟩
     simp_rw [← not_lt]
     contrapose!
     exact clog_pos hb
-  have b_pos : 0 < b := (zero_lt_one' ℕ).trans hb
+  have b_pos : 0 < b := zero_lt_of_lt hb
   rw [clog]; split_ifs with h
-  · rw [succ_eq_add_one, add_le_add_iff_right, ← ih ((x + b - 1) / b) (add_pred_div_lt hb h.2),
-      Nat.div_le_iff_le_mul_add_pred b_pos, mul_comm b, ← Nat.pow_succ,
-      add_tsub_assoc_of_le (Nat.succ_le_of_lt b_pos), add_le_add_iff_right]
-  · exact iff_of_true ((not_lt.1 (not_and.1 h hb)).trans <| succ_le_of_lt <| pow_pos b_pos _)
+  · rw [succ_eq_add_one, Nat.add_le_add_iff_right, ← ih ((x + b - 1) / b) (add_pred_div_lt hb h.2),
+      Nat.div_le_iff_le_mul_add_pred b_pos, Nat.mul_comm b, ← Nat.pow_succ,
+      Nat.add_sub_assoc (Nat.succ_le_of_lt b_pos), Nat.add_le_add_iff_right]
+  · exact iff_of_true ((not_lt.1 (not_and.1 h hb)).trans <| succ_le_of_lt <| Nat.pow_pos b_pos)
       (zero_le _)
 #align nat.le_pow_iff_clog_le Nat.le_pow_iff_clog_le
 
@@ -311,9 +306,7 @@ theorem pow_lt_iff_lt_clog {b : ℕ} (hb : 1 < b) {x y : ℕ} : b ^ y < x ↔ y
 #align nat.pow_lt_iff_lt_clog Nat.pow_lt_iff_lt_clog
 
 theorem clog_pow (b x : ℕ) (hb : 1 < b) : clog b (b ^ x) = x :=
-  eq_of_forall_ge_iff fun z => by
-    rw [← le_pow_iff_clog_le hb]
-    exact (pow_right_strictMono hb).le_iff_le
+  eq_of_forall_ge_iff fun z ↦ by rw [← le_pow_iff_clog_le hb, Nat.pow_le_pow_iff_right hb]
 #align nat.clog_pow Nat.clog_pow
 
 theorem pow_pred_clog_lt_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 1 < x) :
@@ -359,7 +352,7 @@ theorem log_le_clog (b n : ℕ) : log b n ≤ clog b n := by
     rw [log_zero_right]
     exact zero_le _
   | succ n =>
-    exact (pow_right_strictMono hb).le_iff_le.1
+    exact (Nat.pow_le_pow_iff_right hb).1
       ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
 #align nat.log_le_clog Nat.log_le_clog
 
diff --git a/Mathlib/Data/Nat/Order/Basic.lean b/Mathlib/Data/Nat/Order/Basic.lean
index ea530d5ff93be..5b3e1e6d5091f 100644
--- a/Mathlib/Data/Nat/Order/Basic.lean
+++ b/Mathlib/Data/Nat/Order/Basic.lean
@@ -5,22 +5,30 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Algebra.Order.Ring.Canonical
 import Mathlib.Data.Nat.Basic
-import Mathlib.Init.Data.Nat.Bitwise
 
 #align_import data.nat.order.basic from "leanprover-community/mathlib"@"3ed3f98a1e836241990d3d308f1577e434977130"
 
-
 /-!
-# The natural numbers as a linearly ordered commutative semiring
+# Algebraic order instances for the natural numbers
 
-We also have a variety of lemmas which have been deferred from `Data.Nat.Basic` because it is
-easier to prove them with this ordered semiring instance available.
+This file contains algebraic order instances on the natural numbers and a few lemmas about them.
 
-### TODO
+## Implementation note
 
-Move most of the theorems to `Data.Nat.Defs` by modifying their proofs.
--/
+Std has a home-baked development of the algebraic and order theoretic theory of `ℕ` which, in
+particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness libraries
+in mathlib (naturals show up as indices in lists, cardinality in finsets, powers in groups, ...).
+This home-baked development is pursued in `Data.Nat.Defs`.
+
+Less basic uses of `ℕ` should however use the typeclass-mediated development. `Data.Nat.Basic` gives
+access to the algebraic instances. The current file is the one giving access to the algebraic
+order instances.
 
+## TODO
+
+The names of this file, `Data.Nat.Defs` and `Data.Nat.Basic` are archaic and don't match up with
+reality anymore. Rename them.
+-/
 
 universe u v
 
@@ -78,137 +86,6 @@ instance canonicallyOrderedCommSemiring : CanonicallyOrderedCommSemiring ℕ :=
 instance canonicallyLinearOrderedAddCommMonoid : CanonicallyLinearOrderedAddCommMonoid ℕ :=
   { (inferInstance : CanonicallyOrderedAddCommMonoid ℕ), Nat.linearOrder with }
 
-variable {m n k l : ℕ}
-
-/-! ### Equalities and inequalities involving zero and one -/
-
-theorem _root_.NeZero.one_le [NeZero n] : 1 ≤ n := one_le_iff_ne_zero.mpr (NeZero.ne n)
-
-#align nat.mul_ne_zero Nat.mul_ne_zero
-
--- Porting note: already in Std
-#align nat.mul_eq_zero Nat.mul_eq_zero
-
--- Porting note: removing `simp` attribute
-protected theorem zero_eq_mul : 0 = m * n ↔ m = 0 ∨ n = 0 := by rw [eq_comm, Nat.mul_eq_zero]
-#align nat.zero_eq_mul Nat.zero_eq_mul
-
-theorem eq_zero_of_double_le (h : 2 * n ≤ n) : n = 0 :=
-  add_right_eq_self.mp <| le_antisymm ((two_mul n).symm.trans_le h) le_add_self
-#align nat.eq_zero_of_double_le Nat.eq_zero_of_double_le
-
-theorem eq_zero_of_mul_le (hb : 2 ≤ n) (h : n * m ≤ m) : m = 0 :=
-  eq_zero_of_double_le <| le_trans (Nat.mul_le_mul_right _ hb) h
-#align nat.eq_zero_of_mul_le Nat.eq_zero_of_mul_le
-
-#align nat.zero_max Nat.zero_max
-
-@[simp]
-theorem min_eq_zero_iff : min m n = 0 ↔ m = 0 ∨ n = 0 := min_eq_bot
-#align nat.min_eq_zero_iff Nat.min_eq_zero_iff
-
-@[simp]
-theorem max_eq_zero_iff : max m n = 0 ↔ m = 0 ∧ n = 0 := max_eq_bot
-#align nat.max_eq_zero_iff Nat.max_eq_zero_iff
-
-theorem add_eq_max_iff : m + n = max m n ↔ m = 0 ∨ n = 0 := by
-  rw [← min_eq_zero_iff]
-  rcases le_total m n with H | H <;> simp [H]
-#align nat.add_eq_max_iff Nat.add_eq_max_iff
-
-theorem add_eq_min_iff : m + n = min m n ↔ m = 0 ∧ n = 0 := by
-  rw [← max_eq_zero_iff]
-  rcases le_total m n with H | H <;> simp [H]
-#align nat.add_eq_min_iff Nat.add_eq_min_iff
-
-theorem one_le_of_lt (h : n < m) : 1 ≤ m :=
-  lt_of_le_of_lt (Nat.zero_le _) h
-#align nat.one_le_of_lt Nat.one_le_of_lt
-
-theorem eq_one_of_mul_eq_one_right (H : m * n = 1) : m = 1 :=
-  eq_one_of_dvd_one ⟨n, H.symm⟩
-#align nat.eq_one_of_mul_eq_one_right Nat.eq_one_of_mul_eq_one_right
-
-theorem eq_one_of_mul_eq_one_left (H : m * n = 1) : n = 1 :=
-  eq_one_of_mul_eq_one_right (by rwa [mul_comm])
-#align nat.eq_one_of_mul_eq_one_left Nat.eq_one_of_mul_eq_one_left
-
-/-! ### `succ` -/
-
-
-theorem two_le_iff : ∀ n, 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
-  | 0 => by simp
-  | 1 => by simp
-  | n + 2 => by simp
-#align nat.two_le_iff Nat.two_le_iff
-
-@[simp]
-theorem lt_one_iff {n : ℕ} : n < 1 ↔ n = 0 :=
-  Nat.lt_succ_iff.trans nonpos_iff_eq_zero
-#align nat.lt_one_iff Nat.lt_one_iff
-
-/-! ### `add` -/
-
-#align nat.add_pos_left Nat.add_pos_left
-#align nat.add_pos_right Nat.add_pos_right
-
-theorem add_pos_iff_pos_or_pos (m n : ℕ) : 0 < m + n ↔ 0 < m ∨ 0 < n :=
-  Iff.intro
-    (by
-      intro h
-      cases' m with m
-      · simp [zero_add] at h
-        exact Or.inr h
-      exact Or.inl (succ_pos _))
-    (by
-      intro h; cases' h with mpos npos
-      · apply Nat.add_pos_left mpos
-      apply Nat.add_pos_right _ npos)
-#align nat.add_pos_iff_pos_or_pos Nat.add_pos_iff_pos_or_pos
-
-theorem add_eq_one_iff : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 := by
-  cases n <;> simp [succ_eq_add_one, ← add_assoc, succ_inj']
-#align nat.add_eq_one_iff Nat.add_eq_one_iff
-
-theorem add_eq_two_iff : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0 := by
-  omega
-#align nat.add_eq_two_iff Nat.add_eq_two_iff
-
-theorem add_eq_three_iff :
-    m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0 := by
-  omega
-#align nat.add_eq_three_iff Nat.add_eq_three_iff
-
-theorem le_add_one_iff : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1 := by
-  rw [le_iff_lt_or_eq, lt_add_one_iff]
-#align nat.le_add_one_iff Nat.le_add_one_iff
-
-theorem le_and_le_add_one_iff : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1 := by
-  rw [le_add_one_iff, and_or_left, ← le_antisymm_iff, eq_comm, and_iff_right_of_imp]
-  rintro rfl
-  exact n.le_succ
-#align nat.le_and_le_add_one_iff Nat.le_and_le_add_one_iff
-
-theorem add_succ_lt_add (hab : m < n) (hcd : k < l) : m + k + 1 < n + l := by
-  rw [add_assoc]
-  exact add_lt_add_of_lt_of_le hab (Nat.succ_le_iff.2 hcd)
-#align nat.add_succ_lt_add Nat.add_succ_lt_add
-
-/-! ### `pred` -/
-
-
-theorem pred_le_iff : pred m ≤ n ↔ m ≤ succ n :=
-  ⟨le_succ_of_pred_le, by
-    cases m
-    · exact fun _ => zero_le n
-    exact le_of_succ_le_succ⟩
-#align nat.pred_le_iff Nat.pred_le_iff
-
-/-! ### `sub`
-
-Most lemmas come from the `OrderedSub` instance on `ℕ`. -/
-
-
 instance : OrderedSub ℕ := by
   constructor
   intro m n k
@@ -216,514 +93,6 @@ instance : OrderedSub ℕ := by
   · simp
   · simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]
 
-theorem lt_pred_iff : n < pred m ↔ succ n < m :=
-  show n < m - 1 ↔ n + 1 < m from lt_tsub_iff_right
-#align nat.lt_pred_iff Nat.lt_pred_iff
-
-theorem lt_of_lt_pred (h : m < n - 1) : m < n :=
-  lt_of_succ_lt (lt_pred_iff.1 h)
-#align nat.lt_of_lt_pred Nat.lt_of_lt_pred
-
-theorem le_or_le_of_add_eq_add_pred (h : k + l = m + n - 1) : m ≤ k ∨ n ≤ l := by
-  rcases le_or_lt m k with h' | h' <;> [left; right]
-  · exact h'
-  · replace h' := add_lt_add_right h' l
-    rw [h] at h'
-    rcases n.eq_zero_or_pos with hn | hn
-    · rw [hn]
-      exact zero_le l
-    rw [n.add_sub_assoc (Nat.succ_le_of_lt hn), add_lt_add_iff_left] at h'
-    exact Nat.le_of_pred_lt h'
-#align nat.le_or_le_of_add_eq_add_pred Nat.le_or_le_of_add_eq_add_pred
-
-/-- A version of `Nat.sub_succ` in the form `_ - 1` instead of `Nat.pred _`. -/
-theorem sub_succ' (m n : ℕ) : m - n.succ = m - n - 1 :=
-  rfl
-#align nat.sub_succ' Nat.sub_succ'
-
-/-! ### `mul` -/
-
-theorem succ_mul_pos (m : ℕ) (hn : 0 < n) : 0 < succ m * n :=
-  mul_pos (succ_pos m) hn
-#align nat.succ_mul_pos Nat.succ_mul_pos
-
-theorem mul_self_le_mul_self (h : m ≤ n) : m * m ≤ n * n :=
-  mul_le_mul h h (zero_le _) (zero_le _)
-#align nat.mul_self_le_mul_self Nat.mul_self_le_mul_self
-
-theorem mul_self_lt_mul_self : ∀ {m n : ℕ}, m < n → m * m < n * n
-  | 0, _, h => mul_pos h h
-  | succ _, _, h => mul_lt_mul h (le_of_lt h) (succ_pos _) (zero_le _)
-#align nat.mul_self_lt_mul_self Nat.mul_self_lt_mul_self
-
-theorem mul_self_le_mul_self_iff : m ≤ n ↔ m * m ≤ n * n :=
-  ⟨mul_self_le_mul_self, le_imp_le_of_lt_imp_lt mul_self_lt_mul_self⟩
-#align nat.mul_self_le_mul_self_iff Nat.mul_self_le_mul_self_iff
-
-theorem mul_self_lt_mul_self_iff : m < n ↔ m * m < n * n :=
-  le_iff_le_iff_lt_iff_lt.1 mul_self_le_mul_self_iff
-#align nat.mul_self_lt_mul_self_iff Nat.mul_self_lt_mul_self_iff
-
-theorem le_mul_self : ∀ n : ℕ, n ≤ n * n
-  | 0 => le_rfl
-  | n + 1 => by simp
-#align nat.le_mul_self Nat.le_mul_self
-
--- Moved to Std
-#align nat.le_mul_of_pos_left Nat.le_mul_of_pos_left
-
--- Moved to Std
-#align nat.le_mul_of_pos_right Nat.le_mul_of_pos_right
-
-theorem mul_self_inj : m * m = n * n ↔ m = n :=
-  le_antisymm_iff.trans
-    (le_antisymm_iff.trans (and_congr mul_self_le_mul_self_iff mul_self_le_mul_self_iff)).symm
-#align nat.mul_self_inj Nat.mul_self_inj
-
-theorem le_add_pred_of_pos (n : ℕ) {i : ℕ} (hi : i ≠ 0) : n ≤ i + (n - 1) := by
-  refine le_trans ?_ add_tsub_le_assoc
-  simp [add_comm, Nat.add_sub_assoc, one_le_iff_ne_zero.2 hi]
-#align nat.le_add_pred_of_pos Nat.le_add_pred_of_pos
-
-@[simp]
-theorem lt_mul_self_iff : ∀ {n : ℕ}, n < n * n ↔ 1 < n
-  | 0 => iff_of_false (lt_irrefl _) zero_le_one.not_lt
-  | n + 1 => lt_mul_iff_one_lt_left n.succ_pos
-#align nat.lt_mul_self_iff Nat.lt_mul_self_iff
-
-theorem add_sub_one_le_mul (hm : m ≠ 0) (hn : n ≠ 0) : m + n - 1 ≤ m * n := by
-  cases m
-  · cases hm rfl
-  · rw [succ_add, Nat.add_one_sub_one, succ_mul]
-    exact add_le_add_right (le_mul_of_one_le_right' <| succ_le_iff.2 <| pos_iff_ne_zero.2 hn) _
-#align nat.add_sub_one_le_mul Nat.add_sub_one_le_mul
-
-/-!
-### Recursion and induction principles
-
-This section is here due to dependencies -- the lemmas here require some of the lemmas
-proved above, and some of the results in later sections depend on the definitions in this section.
--/
-
-
-/-- Given a predicate on two naturals `P : ℕ → ℕ → Prop`, `P a b` is true for all `a < b` if
-`P (a + 1) (a + 1)` is true for all `a`, `P 0 (b + 1)` is true for all `b` and for all
-`a < b`, `P (a + 1) b` is true and `P a (b + 1)` is true implies `P (a + 1) (b + 1)` is true. -/
-@[elab_as_elim]
-theorem diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ a, P (a + 1) (a + 1)) (hb : ∀ b, P 0 (b + 1))
-    (hd : ∀ a b, a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) : ∀ a b, a < b → P a b
-  | 0, b + 1, _ => hb _
-  | a + 1, b + 1, h => by
-    apply hd _ _ ((add_lt_add_iff_right _).1 h)
-    · have this : a + 1 = b ∨ a + 1 < b := by rwa [← le_iff_eq_or_lt, ← Nat.lt_succ_iff]
-      have wf : (a + 1) + b < (a + 1) + (b + 1) := by simp
-      rcases this with (rfl | h)
-      · exact ha _
-      apply diag_induction P ha hb hd (a + 1) b h
-    have _ : a + (b + 1) < (a + 1) + (b + 1) := by simp
-    apply diag_induction P ha hb hd a (b + 1)
-    apply lt_of_le_of_lt (Nat.le_succ _) h
-  termination_by a b _c => a + b
-  decreasing_by all_goals assumption
-#align nat.diag_induction Nat.diag_induction
-
-/-- A subset of `ℕ` containing `k : ℕ` and closed under `Nat.succ` contains every `n ≥ k`. -/
-theorem set_induction_bounded {S : Set ℕ} (hk : k ∈ S) (h_ind : ∀ k : ℕ, k ∈ S → k + 1 ∈ S)
-    (hnk : k ≤ n) : n ∈ S :=
-  @leRecOn (fun n => n ∈ S) k n hnk @h_ind hk
-#align nat.set_induction_bounded Nat.set_induction_bounded
-
-/-- A subset of `ℕ` containing zero and closed under `Nat.succ` contains all of `ℕ`. -/
-theorem set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ k : ℕ, k ∈ S → k + 1 ∈ S) (n : ℕ) :
-    n ∈ S :=
-  set_induction_bounded hb h_ind (zero_le n)
-#align nat.set_induction Nat.set_induction
-
-/-! ### `div` -/
-
-
-protected theorem div_le_of_le_mul' (h : m ≤ k * n) : m / k ≤ n :=
-  (Nat.eq_zero_or_pos k).elim (fun k0 => by rw [k0, Nat.div_zero]; apply zero_le) fun k0 =>
-    le_of_mul_le_mul_left
-      (calc
-        k * (m / k) ≤ m % k + k * (m / k) := Nat.le_add_left _ _
-        _ = m := mod_add_div _ _
-        _ ≤ k * n := h) k0
-#align nat.div_le_of_le_mul' Nat.div_le_of_le_mul'
-
-protected theorem div_le_self' (m n : ℕ) : m / n ≤ m :=
-  (Nat.eq_zero_or_pos n).elim (fun n0 => by rw [n0, Nat.div_zero]; apply zero_le) fun n0 =>
-    Nat.div_le_of_le_mul' <|
-      calc
-        m = 1 * m := (one_mul _).symm
-        _ ≤ n * m := Nat.mul_le_mul_right _ n0
-#align nat.div_le_self' Nat.div_le_self'
-
-#align nat.div_lt_of_lt_mul Nat.div_lt_of_lt_mul
-
-theorem eq_zero_of_le_div (hn : 2 ≤ n) (h : m ≤ m / n) : m = 0 :=
-  eq_zero_of_mul_le hn <| by
-    rw [mul_comm]; exact (Nat.le_div_iff_mul_le' (lt_of_lt_of_le (by decide) hn)).1 h
-#align nat.eq_zero_of_le_div Nat.eq_zero_of_le_div
-
-theorem div_mul_div_le_div (m n k : ℕ) : m / k * n / m ≤ n / k :=
-  if hm0 : m = 0 then by simp [hm0]
-  else
-    calc
-      m / k * n / m ≤ n * m / k / m :=
-        Nat.div_le_div_right (by rw [mul_comm]; exact mul_div_le_mul_div_assoc _ _ _)
-      _ = n / k := by
-        { rw [Nat.div_div_eq_div_mul, mul_comm n, mul_comm k,
-            Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero hm0)] }
-#align nat.div_mul_div_le_div Nat.div_mul_div_le_div
-
-theorem eq_zero_of_le_half (h : n ≤ n / 2) : n = 0 :=
-  eq_zero_of_le_div le_rfl h
-#align nat.eq_zero_of_le_half Nat.eq_zero_of_le_half
-
-theorem mul_div_mul_comm_of_dvd_dvd (hmk : k ∣ m) (hnl : l ∣ n) :
-    m * n / (k * l) = m / k * (n / l) := by
-  rcases k.eq_zero_or_pos with (rfl | hk0); · simp
-  rcases l.eq_zero_or_pos with (rfl | hl0); · simp
-  obtain ⟨_, rfl⟩ := hmk
-  obtain ⟨_, rfl⟩ := hnl
-  rw [mul_mul_mul_comm, Nat.mul_div_cancel_left _ hk0, Nat.mul_div_cancel_left _ hl0,
-    Nat.mul_div_cancel_left _ (mul_pos hk0 hl0)]
-#align nat.mul_div_mul_comm_of_dvd_dvd Nat.mul_div_mul_comm_of_dvd_dvd
-
-theorem le_half_of_half_lt_sub {a b : ℕ} (h : a / 2 < a - b) : b ≤ a / 2 := by
-  rw [Nat.le_div_iff_mul_le two_pos]
-  rw [Nat.div_lt_iff_lt_mul two_pos, Nat.mul_sub_right_distrib, lt_tsub_iff_right, mul_two a] at h
-  exact le_of_lt (Nat.lt_of_add_lt_add_left h)
-#align nat.le_half_of_half_lt_sub Nat.le_half_of_half_lt_sub
-
-theorem half_le_of_sub_le_half {a b : ℕ} (h : a - b ≤ a / 2) : a / 2 ≤ b := by
-  rw [Nat.le_div_iff_mul_le two_pos, Nat.mul_sub_right_distrib, tsub_le_iff_right, mul_two,
-    add_le_add_iff_left] at h
-  rw [← Nat.mul_div_left b two_pos]
-  exact Nat.div_le_div_right h
-#align nat.half_le_of_sub_le_half Nat.half_le_of_sub_le_half
-
-/-! ### `mod`, `dvd` -/
-
-
-theorem two_mul_odd_div_two (hn : n % 2 = 1) : 2 * (n / 2) = n - 1 := by
-  conv =>
-    rhs
-    rw [← Nat.mod_add_div n 2, hn, @add_tsub_cancel_left]
-#align nat.two_mul_odd_div_two Nat.two_mul_odd_div_two
-
-theorem div_dvd_of_dvd (h : n ∣ m) : m / n ∣ m :=
-  ⟨n, (Nat.div_mul_cancel h).symm⟩
-#align nat.div_dvd_of_dvd Nat.div_dvd_of_dvd
-
-protected theorem div_div_self (h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n := by
-  rcases h with ⟨_, rfl⟩
-  rw [mul_ne_zero_iff] at hm
-  rw [mul_div_right _ (Nat.pos_of_ne_zero hm.1), mul_div_left _ (Nat.pos_of_ne_zero hm.2)]
-#align nat.div_div_self Nat.div_div_self
-
-#align nat.mod_mul_right_div_self Nat.mod_mul_right_div_self
-#align nat.mod_mul_left_div_self Nat.mod_mul_left_div_self
-
-theorem not_dvd_of_pos_of_lt (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n := by
-  rintro ⟨k, rfl⟩
-  rcases Nat.eq_zero_or_pos k with (rfl | hk)
-  · exact lt_irrefl 0 h1
-  · exact not_lt.2 (Nat.le_mul_of_pos_right _ hk) h2
-#align nat.not_dvd_of_pos_of_lt Nat.not_dvd_of_pos_of_lt
-
-/-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`. -/
-theorem sub_mod_eq_zero_of_mod_eq (h : m % k = n % k) : (m - n) % k = 0 := by
-  rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, tsub_add_eq_tsub_tsub,
-    @add_tsub_cancel_left, ← mul_tsub k, Nat.mul_mod_right]
-#align nat.sub_mod_eq_zero_of_mod_eq Nat.sub_mod_eq_zero_of_mod_eq
-
-@[simp]
-theorem one_mod (n : ℕ) : 1 % (n + 2) = 1 :=
-  Nat.mod_eq_of_lt (add_lt_add_right n.succ_pos 1)
-#align nat.one_mod Nat.one_mod
-
-theorem one_mod_of_ne_one : ∀ {n : ℕ}, n ≠ 1 → 1 % n = 1
-  | 0, _ | (n + 2), _ => by simp
-
-theorem dvd_sub_mod (k : ℕ) : n ∣ k - k % n :=
-  ⟨k / n, tsub_eq_of_eq_add_rev (Nat.mod_add_div k n).symm⟩
-#align nat.dvd_sub_mod Nat.dvd_sub_mod
-
-theorem add_mod_eq_ite :
-    (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k := by
-  cases k; simp only [zero_eq, mod_zero, _root_.zero_le, ↓reduceIte, tsub_zero]
-  rw [Nat.add_mod]
-  split_ifs with h
-  · rw [Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]
-    exact
-      (tsub_lt_iff_right h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _))
-        (n.mod_lt (zero_lt_succ _)))
-  · exact Nat.mod_eq_of_lt (lt_of_not_ge h)
-#align nat.add_mod_eq_ite Nat.add_mod_eq_ite
-
-theorem div_eq_self : m / n = m ↔ m = 0 ∨ n = 1 := by
-  constructor
-  · intro
-    match n with
-    | 0 => simp_all
-    | 1 =>
-      right
-      rfl
-    | n+2 =>
-      left
-      have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)
-      refine eq_zero_of_le_half ?_
-      simp_all
-  · rintro (rfl | rfl) <;> simp
-#align nat.div_eq_self Nat.div_eq_self
-
-theorem div_eq_sub_mod_div : m / n = (m - m % n) / n := by
-  by_cases n0 : n = 0
-  · rw [n0, Nat.div_zero, Nat.div_zero]
-  · have : m - m % n = n * (m / n) := by
-      rw [tsub_eq_iff_eq_add_of_le (Nat.mod_le _ _), add_comm, mod_add_div]
-    rw [this, mul_div_right _ (Nat.pos_of_ne_zero n0)]
-#align nat.div_eq_sub_mod_div Nat.div_eq_sub_mod_div
-
-/-- `m` is not divisible by `n` if it is between `n * k` and `n * (k + 1)` for some `k`. -/
-theorem not_dvd_of_between_consec_multiples (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m := by
-  rintro ⟨d, rfl⟩
-  exact Monotone.ne_of_lt_of_lt_nat (Covariant.monotone_of_const n) k h1 h2 d rfl
-#align nat.not_dvd_of_between_consec_multiples Nat.not_dvd_of_between_consec_multiples
-
-/-! ### `find` -/
-
-
-section Find
-
-variable {p q : ℕ → Prop} [DecidablePred p] [DecidablePred q]
-
--- Porting note (#10618): removing `simp` attribute as `simp` can prove it
-theorem find_pos (h : ∃ n : ℕ, p n) : 0 < Nat.find h ↔ ¬p 0 := by
-  rw [pos_iff_ne_zero, Ne, Nat.find_eq_zero]
-#align nat.find_pos Nat.find_pos
-
-theorem find_add {hₘ : ∃ m, p (m + n)} {hₙ : ∃ n, p n} (hn : n ≤ Nat.find hₙ) :
-    Nat.find hₘ + n = Nat.find hₙ := by
-  refine ((le_find_iff _ _).2 fun m hm hpm => hm.not_le ?_).antisymm ?_
-  · have hnm : n ≤ m := hn.trans (find_le hpm)
-    refine add_le_of_le_tsub_right_of_le hnm (find_le ?_)
-    rwa [tsub_add_cancel_of_le hnm]
-  · rw [← tsub_le_iff_right]
-    refine (le_find_iff _ _).2 fun m hm hpm => hm.not_le ?_
-    rw [tsub_le_iff_right]
-    exact find_le hpm
-#align nat.find_add Nat.find_add
-
-end Find
-
-/-! ### `find_greatest` -/
-
-
-section FindGreatest
-
-variable {P Q : ℕ → Prop} [DecidablePred P]
-
-theorem findGreatest_eq_iff :
-    Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n⦄, m < n → n ≤ k → ¬P n := by
-  induction' k with k ihk generalizing m
-  · rw [eq_comm, Iff.comm]
-    simp only [zero_eq, nonpos_iff_eq_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
-    rintro rfl
-    exact ⟨fun h => (h rfl).elim, fun n hlt heq => (hlt.ne heq.symm).elim⟩
-  · by_cases hk : P (k + 1)
-    · rw [findGreatest_eq hk]
-      constructor
-      · rintro rfl
-        exact ⟨le_rfl, fun _ => hk, fun n hlt hle => (hlt.not_le hle).elim⟩
-      · rintro ⟨hle, h0, hm⟩
-        rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt)
-        exacts [rfl, (hm hlt le_rfl hk).elim]
-    · rw [findGreatest_of_not hk, ihk]
-      constructor
-      · rintro ⟨hle, hP, hm⟩
-        refine ⟨hle.trans k.le_succ, hP, fun n hlt hle => ?_⟩
-        rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt')
-        exacts [hk, hm hlt <| Nat.lt_succ_iff.1 hlt']
-      · rintro ⟨hle, hP, hm⟩
-        refine ⟨Nat.lt_succ_iff.1 (hle.lt_of_ne ?_), hP,
-          fun n hlt hle => hm hlt (hle.trans k.le_succ)⟩
-        rintro rfl
-        exact hk (hP k.succ_ne_zero)
-#align nat.find_greatest_eq_iff Nat.findGreatest_eq_iff
-
-theorem findGreatest_eq_zero_iff : Nat.findGreatest P k = 0 ↔ ∀ ⦃n⦄, 0 < n → n ≤ k → ¬P n := by
-  simp [findGreatest_eq_iff]
-#align nat.find_greatest_eq_zero_iff Nat.findGreatest_eq_zero_iff
-
-@[simp] lemma findGreatest_pos : 0 < Nat.findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n := by
-  rw [pos_iff_ne_zero, Ne.def, findGreatest_eq_zero_iff]; push_neg; rfl
-
-theorem findGreatest_spec (hmb : m ≤ n) (hm : P m) : P (Nat.findGreatest P n) := by
-  by_cases h : Nat.findGreatest P n = 0
-  · cases m
-    · rwa [h]
-    exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim
-  · exact (findGreatest_eq_iff.1 rfl).2.1 h
-#align nat.find_greatest_spec Nat.findGreatest_spec
-
-theorem findGreatest_le (n : ℕ) : Nat.findGreatest P n ≤ n :=
-  (findGreatest_eq_iff.1 rfl).1
-#align nat.find_greatest_le Nat.findGreatest_le
-
-theorem le_findGreatest (hmb : m ≤ n) (hm : P m) : m ≤ Nat.findGreatest P n :=
-  le_of_not_lt fun hlt => (findGreatest_eq_iff.1 rfl).2.2 hlt hmb hm
-#align nat.le_find_greatest Nat.le_findGreatest
-
-theorem findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] :
-    Monotone (Nat.findGreatest P) := by
-  refine monotone_nat_of_le_succ fun n => ?_
-  rw [findGreatest_succ]
-  split_ifs
-  · exact (findGreatest_le n).trans (le_succ _)
-  · rfl
-#align nat.find_greatest_mono_right Nat.findGreatest_mono_right
-
-theorem findGreatest_mono_left [DecidablePred Q] (hPQ : P ≤ Q) :
-    Nat.findGreatest P ≤ Nat.findGreatest Q := by
-  intro n
-  induction' n with n hn
-  · rfl
-  by_cases h : P (n + 1)
-  · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
-  · rw [findGreatest_of_not h]
-    exact hn.trans (Nat.findGreatest_mono_right _ <| le_succ _)
-#align nat.find_greatest_mono_left Nat.findGreatest_mono_left
-
-theorem findGreatest_mono [DecidablePred Q] (hPQ : P ≤ Q) (hmn : m ≤ n) :
-    Nat.findGreatest P m ≤ Nat.findGreatest Q n :=
-  (Nat.findGreatest_mono_right _ hmn).trans <| findGreatest_mono_left hPQ _
-#align nat.find_greatest_mono Nat.findGreatest_mono
-
-theorem findGreatest_is_greatest (hk : Nat.findGreatest P n < k) (hkb : k ≤ n) : ¬P k :=
-  (findGreatest_eq_iff.1 rfl).2.2 hk hkb
-#align nat.find_greatest_is_greatest Nat.findGreatest_is_greatest
-
-theorem findGreatest_of_ne_zero (h : Nat.findGreatest P n = m) (h0 : m ≠ 0) : P m :=
-  (findGreatest_eq_iff.1 h).2.1 h0
-#align nat.find_greatest_of_ne_zero Nat.findGreatest_of_ne_zero
-
-end FindGreatest
-
-/-! ### `bit0` and `bit1` -/
-section Bit
-
-set_option linter.deprecated false
-
-protected theorem bit0_le {n m : ℕ} (h : n ≤ m) : bit0 n ≤ bit0 m :=
-  add_le_add h h
-#align nat.bit0_le Nat.bit0_le
-
-protected theorem bit1_le {n m : ℕ} (h : n ≤ m) : bit1 n ≤ bit1 m :=
-  succ_le_succ (add_le_add h h)
-#align nat.bit1_le Nat.bit1_le
-
-theorem bit_le : ∀ (b : Bool) {m n : ℕ}, m ≤ n → bit b m ≤ bit b n
-  | true, _, _, h => Nat.bit1_le h
-  | false, _, _, h => Nat.bit0_le h
-#align nat.bit_le Nat.bit_le
-
-theorem bit0_le_bit : ∀ (b) {m n : ℕ}, m ≤ n → bit0 m ≤ bit b n
-  | true, _, _, h => le_of_lt <| Nat.bit0_lt_bit1 h
-  | false, _, _, h => Nat.bit0_le h
-#align nat.bit0_le_bit Nat.bit0_le_bit
-
-theorem bit_le_bit1 : ∀ (b) {m n : ℕ}, m ≤ n → bit b m ≤ bit1 n
-  | false, _, _, h => le_of_lt <| Nat.bit0_lt_bit1 h
-  | true, _, _, h => Nat.bit1_le h
-#align nat.bit_le_bit1 Nat.bit_le_bit1
-
-theorem bit_lt_bit0 : ∀ (b) {m n : ℕ}, m < n → bit b m < bit0 n
-  | true, _, _, h => Nat.bit1_lt_bit0 h
-  | false, _, _, h => Nat.bit0_lt h
-#align nat.bit_lt_bit0 Nat.bit_lt_bit0
-
-theorem bit_lt_bit (a b) (h : m < n) : bit a m < bit b n :=
-  lt_of_lt_of_le (bit_lt_bit0 _ h) (bit0_le_bit _ le_rfl)
-#align nat.bit_lt_bit Nat.bit_lt_bit
-
-@[simp]
-theorem bit0_le_bit1_iff : bit0 m ≤ bit1 n ↔ m ≤ n :=
-  ⟨fun h => by
-    rwa [← Nat.lt_succ_iff, n.bit1_eq_succ_bit0,
-    ← n.bit0_succ_eq, bit0_lt_bit0, Nat.lt_succ_iff] at h,
-    fun h => le_of_lt (Nat.bit0_lt_bit1 h)⟩
-#align nat.bit0_le_bit1_iff Nat.bit0_le_bit1_iff
-
-@[simp]
-theorem bit0_lt_bit1_iff : bit0 m < bit1 n ↔ m ≤ n :=
-  ⟨fun h => bit0_le_bit1_iff.1 (le_of_lt h), Nat.bit0_lt_bit1⟩
-#align nat.bit0_lt_bit1_iff Nat.bit0_lt_bit1_iff
-
-@[simp]
-theorem bit1_le_bit0_iff : bit1 m ≤ bit0 n ↔ m < n :=
-  ⟨fun h => by rwa [m.bit1_eq_succ_bit0, succ_le_iff, bit0_lt_bit0] at h, fun h =>
-    le_of_lt (Nat.bit1_lt_bit0 h)⟩
-#align nat.bit1_le_bit0_iff Nat.bit1_le_bit0_iff
-
-@[simp]
-theorem bit1_lt_bit0_iff : bit1 m < bit0 n ↔ m < n :=
-  ⟨fun h => bit1_le_bit0_iff.1 (le_of_lt h), Nat.bit1_lt_bit0⟩
-#align nat.bit1_lt_bit0_iff Nat.bit1_lt_bit0_iff
-
--- Porting note: temporarily porting only needed portions
-/-
-@[simp]
-theorem one_le_bit0_iff : 1 ≤ bit0 n ↔ 0 < n := by
-  convert bit1_le_bit0_iff
-  rfl
-#align nat.one_le_bit0_iff Nat.one_le_bit0_iff
-
-@[simp]
-theorem one_lt_bit0_iff : 1 < bit0 n ↔ 1 ≤ n := by
-  convert bit1_lt_bit0_iff
-  rfl
-#align nat.one_lt_bit0_iff Nat.one_lt_bit0_iff
-
-@[simp]
-theorem bit_le_bit_iff : ∀ {b : Bool}, bit b m ≤ bit b n ↔ m ≤ n
-  | false => bit0_le_bit0
-  | true => bit1_le_bit1
-#align nat.bit_le_bit_iff Nat.bit_le_bit_iff
-
-@[simp]
-theorem bit_lt_bit_iff : ∀ {b : Bool}, bit b m < bit b n ↔ m < n
-  | false => bit0_lt_bit0
-  | true => bit1_lt_bit1
-#align nat.bit_lt_bit_iff Nat.bit_lt_bit_iff
-
-@[simp]
-theorem bit_le_bit1_iff : ∀ {b : Bool}, bit b m ≤ bit1 n ↔ m ≤ n
-  | false => bit0_le_bit1_iff
-  | true => bit1_le_bit1
-#align nat.bit_le_bit1_iff Nat.bit_le_bit1_iff
--/
-
-end Bit
-
-/-! ### decidability of predicates -/
-
-
-instance decidableLoHi (lo hi : ℕ) (P : ℕ → Prop) [H : DecidablePred P] :
-    Decidable (∀ x, lo ≤ x → x < hi → P x) :=
-  decidable_of_iff (∀ x < hi - lo, P (lo + x))
-    ⟨fun al x hl hh => by
-      have := al (x - lo) ((tsub_lt_tsub_iff_right hl).mpr hh)
-      rwa [add_tsub_cancel_of_le hl] at this, fun al x h =>
-      al _ (Nat.le_add_right _ _) (lt_tsub_iff_left.mp h)⟩
-#align nat.decidable_lo_hi Nat.decidableLoHi
-
-instance decidableLoHiLe (lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] :
-    Decidable (∀ x, lo ≤ x → x ≤ hi → P x) :=
-  decidable_of_iff (∀ x, lo ≤ x → x < hi + 1 → P x) <|
-    ball_congr fun _ _ => imp_congr Nat.lt_succ_iff Iff.rfl
-#align nat.decidable_lo_hi_le Nat.decidableLoHiLe
+theorem _root_.NeZero.one_le {n : ℕ} [NeZero n] : 1 ≤ n := one_le_iff_ne_zero.mpr (NeZero.ne n)
 
 end Nat
diff --git a/Mathlib/Data/Nat/Pow.lean b/Mathlib/Data/Nat/Pow.lean
deleted file mode 100644
index 253f0afe92deb..0000000000000
--- a/Mathlib/Data/Nat/Pow.lean
+++ /dev/null
@@ -1,179 +0,0 @@
-/-
-Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
-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.Algebra.GroupPower.Order
-
-#align_import data.nat.pow from "leanprover-community/mathlib"@"3e00d81bdcbf77c8188bbd18f5524ddc3ed8cac6"
-
-/-! # `Nat.pow`
-
-Results on the power operation on natural numbers.
--/
-
-
-namespace Nat
-variable {m n x y : ℕ}
-
-/-! ### `pow` -/
-
--- Porting note: the next two lemmas have moved into `Std`.
--- TODO: Rename `Nat.pow_le_pow_of_le_left` to `Nat.pow_le_pow_left`, protect it, remove the alias
--- TODO: Rename `Nat.pow_le_pow_of_le_right` to `Nat.pow_le_pow_right`, protect it, remove the alias
-
--- The global `pow_le_pow_left` needs an extra hypothesis `0 ≤ x`.
-
-#align nat.pow_le_pow_of_le_left Nat.pow_le_pow_left
-#align nat.pow_le_pow_of_le_right Nat.pow_le_pow_right
-
-protected theorem pow_lt_pow_left (h : x < y) (hn : n ≠ 0) : x ^ n < y ^ n :=
-  pow_lt_pow_left h (zero_le _) hn
-#align nat.pow_lt_pow_of_lt_left Nat.pow_lt_pow_left
-
-#align nat.pow_lt_pow_of_lt_right pow_lt_pow_right
-#align nat.pow_lt_pow_succ Nat.pow_lt_pow_succ
-
-theorem le_self_pow {n : ℕ} (hn : n ≠ 0) : ∀ m : ℕ, m ≤ m ^ n
-  | 0 => zero_le _
-  | (_ + 1) => _root_.le_self_pow (le_add_left _ _) hn
-#align nat.le_self_pow Nat.le_self_pow
-
-theorem lt_pow_self {p : ℕ} (h : 1 < p) : ∀ n : ℕ, n < p ^ n
-  | 0 => by simp [zero_lt_one]
-  | n + 1 =>
-    calc
-      n + 1 < p ^ n + 1 := Nat.add_lt_add_right (lt_pow_self h _) _
-      _ ≤ p ^ (n + 1) := Nat.pow_lt_pow_succ h
-#align nat.lt_pow_self Nat.lt_pow_self
-
-theorem lt_two_pow (n : ℕ) : n < 2 ^ n :=
-  lt_pow_self (by decide) n
-#align nat.lt_two_pow Nat.lt_two_pow
-
-theorem one_le_pow (n m : ℕ) (h : 0 < m) : 1 ≤ m ^ n := by
-  rw [← one_pow n]
-  exact Nat.pow_le_pow_of_le_left h n
-#align nat.one_le_pow Nat.one_le_pow
-
-theorem one_le_pow' (n m : ℕ) : 1 ≤ (m + 1) ^ n :=
-  one_le_pow n (m + 1) (succ_pos m)
-#align nat.one_le_pow' Nat.one_le_pow'
-
-#align nat.one_le_two_pow Nat.one_le_two_pow
-
-theorem one_lt_pow (n m : ℕ) (h₀ : n ≠ 0) (h₁ : 1 < m) : 1 < m ^ n := by
-  rw [← one_pow n]
-  exact Nat.pow_lt_pow_left h₁ h₀
-#align nat.one_lt_pow Nat.one_lt_pow
-
-theorem two_pow_succ (n : ℕ) : 2^(n + 1) = 2^n + 2^n := by simp [Nat.pow_succ, mul_two]
-
-theorem one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) :=
-  one_lt_pow (n + 1) (m + 2) n.succ_ne_zero (Nat.lt_of_sub_eq_succ rfl)
-#align nat.one_lt_pow' Nat.one_lt_pow'
-
-@[simp]
-theorem one_lt_pow_iff {k n : ℕ} (h : k ≠ 0) : 1 < n ^ k ↔ 1 < n :=
-  one_lt_pow_iff_of_nonneg (zero_le _) h
-#align nat.one_lt_pow_iff Nat.one_lt_pow_iff
-
-#align nat.one_lt_two_pow Nat.one_lt_two_pow
-
-theorem one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1) :=
-  one_lt_pow (n + 1) 2 n.succ_ne_zero (by decide)
-#align nat.one_lt_two_pow' Nat.one_lt_two_pow'
-
-#align nat.pow_right_strict_mono pow_right_strictMono
-#align nat.pow_le_iff_lt_right pow_le_pow_iff_right
-#align nat.pow_lt_iff_lt_right pow_lt_pow_iff_right
-
-protected lemma pow_right_injective (hx : 2 ≤ x) : Function.Injective (x ^ ·) :=
-  StrictMono.injective (pow_right_strictMono hx)
-#align nat.pow_right_injective Nat.pow_right_injective
-
-/-- See also `pow_left_strictMonoOn`. -/
-protected theorem pow_left_strictMono (hn : n ≠ 0) : StrictMono (. ^ n : ℕ → ℕ) :=
-  fun _ _ h ↦ Nat.pow_lt_pow_left h hn
-#align nat.pow_left_strict_mono Nat.pow_left_strictMono
-
-theorem mul_lt_mul_pow_succ {n a q : ℕ} (a0 : 0 < a) (q1 : 1 < q) : n * q < a * q ^ (n + 1) := by
-  rw [Nat.pow_succ, ← mul_assoc, mul_lt_mul_right (zero_lt_one.trans q1)]
-  exact lt_mul_of_one_le_of_lt (Nat.succ_le_iff.mpr a0) (Nat.lt_pow_self q1 n)
-#align nat.mul_lt_mul_pow_succ Nat.mul_lt_mul_pow_succ
-
-theorem _root_.StrictMono.nat_pow {n : ℕ} (hn : n ≠ 0) {f : ℕ → ℕ} (hf : StrictMono f) :
-    StrictMono fun m => f m ^ n :=
-  (Nat.pow_left_strictMono hn).comp hf
-#align strict_mono.nat_pow StrictMono.nat_pow
-
-protected theorem pow_le_pow_iff_left (hm : m ≠ 0) : x ^ m ≤ y ^ m ↔ x ≤ y :=
-  pow_le_pow_iff_left (zero_le _) (zero_le _) hm
-#align nat.pow_le_iff_le_left Nat.pow_le_pow_iff_left
-
-protected theorem pow_lt_pow_iff_left (hm : m ≠ 0) : x ^ m < y ^ m ↔ x < y :=
-  pow_lt_pow_iff_left (zero_le _) (zero_le _) hm
-#align nat.pow_lt_iff_lt_left Nat.pow_lt_pow_iff_left
-
-theorem pow_left_injective (hm : m ≠ 0) : Function.Injective fun x : ℕ => x ^ m :=
-  (Nat.pow_left_strictMono hm).injective
-#align nat.pow_left_injective Nat.pow_left_injective
-
-theorem sq_sub_sq (a b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
-  rw [sq, sq]
-  exact Nat.mul_self_sub_mul_self_eq a b
-#align nat.sq_sub_sq Nat.sq_sub_sq
-
-alias pow_two_sub_pow_two := sq_sub_sq
-#align nat.pow_two_sub_pow_two Nat.pow_two_sub_pow_two
-
-/-! ### `pow` and `mod` / `dvd` -/
-
-
-theorem pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n := by
-  induction' b with b ih
-  rfl; simp [pow_succ, Nat.mul_mod, ih]
-#align nat.pow_mod Nat.pow_mod
-
-#align nat.mod_pow_succ Nat.mod_pow_succ
-#align nat.pow_dvd_pow_iff_pow_le_pow Nat.pow_dvd_pow_iff_pow_le_pow
-#align nat.pow_dvd_pow_iff_le_right Nat.pow_dvd_pow_iff_le_right
-#align nat.pow_dvd_pow_iff_le_right' Nat.pow_dvd_pow_iff_le_right'
-
-theorem not_pos_pow_dvd : ∀ {p k : ℕ} (_ : 1 < p) (_ : 1 < k), ¬p ^ k ∣ p
-  | succ p, succ k, hp, hk, h =>
-    have : succ p * succ p ^ k ∣ succ p * 1 := by simpa [pow_succ'] using h
-    have : succ p ^ k ∣ 1 := Nat.dvd_of_mul_dvd_mul_left (succ_pos _) this
-    have he : succ p ^ k = 1 := eq_one_of_dvd_one this
-    have : k < succ p ^ k := lt_pow_self hp k
-    have : k < 1 := by rwa [he] at this
-    have : k = 0 := Nat.eq_zero_of_le_zero <| le_of_lt_succ this
-    have : 1 < 1 := by rwa [this] at hk
-    absurd this (by decide)
-#align nat.not_pos_pow_dvd Nat.not_pos_pow_dvd
-
-#align nat.pow_dvd_of_le_of_pow_dvd Nat.pow_dvd_of_le_of_pow_dvd
-#align nat.dvd_of_pow_dvd Nat.dvd_of_pow_dvd
-#align nat.pow_div Nat.pow_div
-
-theorem lt_of_pow_dvd_right {p i n : ℕ} (hn : n ≠ 0) (hp : 2 ≤ p) (h : p ^ i ∣ n) : i < n := by
-  rw [← pow_lt_pow_iff_right (succ_le_iff.1 hp)]
-  exact lt_of_le_of_lt (le_of_dvd hn.bot_lt h) (lt_pow_self (succ_le_iff.mp hp) n)
-#align nat.lt_of_pow_dvd_right Nat.lt_of_pow_dvd_right
-
-end Nat
-
-/-!
-### Deprecated lemmas
-
-Those lemmas have been deprecated on 2023-12-23.
--/
-
-@[deprecated] alias Nat.pow_lt_pow_of_lt_left := Nat.pow_lt_pow_left
-@[deprecated] alias Nat.pow_le_iff_le_left := Nat.pow_le_pow_iff_left
-@[deprecated] alias Nat.pow_lt_pow_of_lt_right := pow_lt_pow_right
-@[deprecated] protected alias Nat.pow_right_strictMono := pow_right_strictMono
-@[deprecated] alias Nat.pow_le_iff_le_right := pow_le_pow_iff_right
-@[deprecated] alias Nat.pow_lt_iff_lt_right := pow_lt_pow_iff_right
-
-assert_not_exists Set.range
diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index 59c36b011c180..b70a61eff0dbb 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -4,7 +4,7 @@ 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.Data.Nat.Bits
-import Mathlib.Algebra.GroupPower.Order
+import Mathlib.Order.Lattice
 
 #align_import data.nat.size from "leanprover-community/mathlib"@"18a5306c091183ac90884daa9373fa3b178e8607"
 
@@ -93,9 +93,7 @@ theorem size_shiftLeft' {b m n} (h : shiftLeft' b m n ≠ 0) :
   rw [shiftLeft'_tt_eq_mul_pow] at this
   obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
   simp only [zero_add, one_mul] at this
-  obtain rfl : n = 0 :=
-    Nat.eq_zero_of_le_zero
-      (le_of_not_gt fun hn => ne_of_gt (pow_lt_pow_right (by decide) hn) this)
+  obtain rfl : n = 0 := not_ne_iff.1 fun hn ↦ ne_of_gt (Nat.one_lt_pow hn (by decide)) this
   rfl
 #align nat.size_shiftl' Nat.size_shiftLeft'
 
@@ -131,7 +129,7 @@ theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
       cases' n with n
       · exact e.elim (Nat.eq_zero_of_le_zero (le_of_lt_succ h))
       · apply succ_le_succ (IH _)
-        apply lt_of_mul_lt_mul_left _ (zero_le 2)
+        apply Nat.lt_of_mul_lt_mul_left (a := 2)
         simp only [← bit0_val, shiftLeft_succ] at *
         exact lt_of_le_of_lt (bit0_le_bit b rfl.le) h⟩
 #align nat.size_le Nat.size_le
@@ -144,11 +142,11 @@ theorem size_pos {n : ℕ} : 0 < size n ↔ 0 < n := by rw [lt_size]; rfl
 #align nat.size_pos Nat.size_pos
 
 theorem size_eq_zero {n : ℕ} : size n = 0 ↔ n = 0 := by
-  have h := @size_pos n; simp only [pos_iff_ne_zero, ne_eq] at h; exact Decidable.not_iff_not.1 h
+  simpa [Nat.pos_iff_ne_zero, not_iff_not] using size_pos
 #align nat.size_eq_zero Nat.size_eq_zero
 
 theorem size_pow {n : ℕ} : size (2 ^ n) = n + 1 :=
-  le_antisymm (size_le.2 <| pow_lt_pow_right (by decide) (lt_succ_self _))
+  le_antisymm (size_le.2 <| Nat.pow_lt_pow_right (by decide) (lt_succ_self _))
     (lt_size.2 <| le_rfl)
 #align nat.size_pow Nat.size_pow
 
diff --git a/Mathlib/Data/Nat/Sqrt.lean b/Mathlib/Data/Nat/Sqrt.lean
index c424718679562..a428cfa873e25 100644
--- a/Mathlib/Data/Nat/Sqrt.lean
+++ b/Mathlib/Data/Nat/Sqrt.lean
@@ -83,7 +83,7 @@ theorem sqrt_le_add (n : ℕ) : n ≤ sqrt n * sqrt n + sqrt n + sqrt n := by
 
 theorem le_sqrt {m n : ℕ} : m ≤ sqrt n ↔ m * m ≤ n :=
   ⟨fun h => le_trans (mul_self_le_mul_self h) (sqrt_le n),
-   fun h => le_of_lt_succ <| mul_self_lt_mul_self_iff.2 <| lt_of_le_of_lt h (lt_succ_sqrt n)⟩
+    fun h => le_of_lt_succ <| Nat.mul_self_lt_mul_self_iff.1 <| lt_of_le_of_lt h (lt_succ_sqrt n)⟩
 #align nat.le_sqrt Nat.le_sqrt
 
 theorem le_sqrt' {m n : ℕ} : m ≤ sqrt n ↔ m ^ 2 ≤ n := by simpa only [pow_two] using le_sqrt
@@ -201,8 +201,8 @@ theorem succ_le_succ_sqrt' (n : ℕ) : n + 1 ≤ (sqrt n + 1) ^ 2 :=
 theorem not_exists_sq {n m : ℕ} (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) :
     ¬∃ t, t * t = n := by
   rintro ⟨t, rfl⟩
-  have h1 : m < t := Nat.mul_self_lt_mul_self_iff.mpr hl
-  have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.mpr hr
+  have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl
+  have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.1 hr
   exact (not_lt_of_ge <| le_of_lt_succ h2) h1
 #align nat.not_exists_sq Nat.not_exists_sq
 
diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean
index 84494e1f159fc..d0d2147b957e1 100644
--- a/Mathlib/Data/Nat/Squarefree.lean
+++ b/Mathlib/Data/Nat/Squarefree.lean
@@ -350,7 +350,7 @@ theorem sq_mul_squarefree_of_pos {n : ℕ} (hn : 0 < n) :
   refine' Nat.lt_le_asymm _ (Finset.le_max' S ((b * x) ^ 2) _)
   -- Porting note: these two goals were in the opposite order in Lean 3
   · convert lt_mul_of_one_lt_right hlts
-      (one_lt_pow 2 x two_ne_zero (one_lt_iff_ne_zero_and_ne_one.mpr ⟨fun h => by simp_all, hx⟩))
+      (one_lt_pow two_ne_zero (one_lt_iff_ne_zero_and_ne_one.mpr ⟨fun h => by simp_all, hx⟩))
       using 1
     rw [mul_pow]
   · simp_rw [S, hsa, Finset.mem_filter, Finset.mem_range]
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
index eabc21a364869..2b330062a44d2 100644
--- a/Mathlib/FieldTheory/Finite/Basic.lean
+++ b/Mathlib/FieldTheory/Finite/Basic.lean
@@ -333,7 +333,7 @@ set_option linter.uppercaseLean3 false in
 
 theorem X_pow_card_pow_sub_X_natDegree_eq (hn : n ≠ 0) (hp : 1 < p) :
     (X ^ p ^ n - X : K'[X]).natDegree = p ^ n :=
-  X_pow_card_sub_X_natDegree_eq K' <| Nat.one_lt_pow _ _ hn hp
+  X_pow_card_sub_X_natDegree_eq K' <| Nat.one_lt_pow hn hp
 set_option linter.uppercaseLean3 false in
 #align finite_field.X_pow_card_pow_sub_X_nat_degree_eq FiniteField.X_pow_card_pow_sub_X_natDegree_eq
 
@@ -346,7 +346,7 @@ set_option linter.uppercaseLean3 false in
 #align finite_field.X_pow_card_sub_X_ne_zero FiniteField.X_pow_card_sub_X_ne_zero
 
 theorem X_pow_card_pow_sub_X_ne_zero (hn : n ≠ 0) (hp : 1 < p) : (X ^ p ^ n - X : K'[X]) ≠ 0 :=
-  X_pow_card_sub_X_ne_zero K' <| Nat.one_lt_pow _ _ hn hp
+  X_pow_card_sub_X_ne_zero K' <| Nat.one_lt_pow hn hp
 set_option linter.uppercaseLean3 false in
 #align finite_field.X_pow_card_pow_sub_X_ne_zero FiniteField.X_pow_card_pow_sub_X_ne_zero
 
diff --git a/Mathlib/NumberTheory/FLT/Four.lean b/Mathlib/NumberTheory/FLT/Four.lean
index 89fa97db9fbf0..69062c24f1178 100644
--- a/Mathlib/NumberTheory/FLT/Four.lean
+++ b/Mathlib/NumberTheory/FLT/Four.lean
@@ -101,7 +101,7 @@ theorem coprime_of_minimal {a b c : ℤ} (h : Minimal a b c) : IsCoprime a b :=
     (Fermat42.mul (Int.coe_nat_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1
   apply Nat.le_lt_asymm (h.2 _ _ _ hf)
   rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_ofNat]
-  · exact Nat.one_lt_pow _ _ two_ne_zero (Nat.Prime.one_lt hp)
+  · exact Nat.one_lt_pow two_ne_zero (Nat.Prime.one_lt hp)
   · exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))
 #align fermat_42.coprime_of_minimal Fermat42.coprime_of_minimal
 
diff --git a/Mathlib/NumberTheory/FermatPsp.lean b/Mathlib/NumberTheory/FermatPsp.lean
index 5e70004d5e0ac..8df20c14b1710 100644
--- a/Mathlib/NumberTheory/FermatPsp.lean
+++ b/Mathlib/NumberTheory/FermatPsp.lean
@@ -153,8 +153,7 @@ private theorem AB_id_helper (b p : ℕ) (_ : 2 ≤ b) (hp : Odd p) :
   have q₁ : b - 1 ∣ b ^ p - 1 := by simpa only [one_pow] using nat_sub_dvd_pow_sub_pow b 1 p
   have q₂ : b + 1 ∣ b ^ p + 1 := by simpa only [one_pow] using hp.nat_add_dvd_pow_add_pow b 1
   convert Nat.div_mul_div_comm q₁ q₂ using 2 <;> rw [mul_comm (_ - 1), ← Nat.sq_sub_sq]
-  · ring_nf
-  · simp
+  ring_nf
 
 /-- Used in the proof of `psp_from_prime_psp`
 -/
diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean
index 3aac9a1203fb5..d21a87375d1d5 100644
--- a/Mathlib/NumberTheory/Padics/PadicVal.lean
+++ b/Mathlib/NumberTheory/Padics/PadicVal.lean
@@ -640,7 +640,7 @@ theorem range_pow_padicValNat_subset_divisors' {n : ℕ} [hp : Fact p.Prime] :
   obtain ⟨k, hk, rfl⟩ := ht
   rw [Finset.mem_erase, Nat.mem_divisors]
   refine' ⟨_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩
-  exact (Nat.one_lt_pow _ _ k.succ_ne_zero hp.out.one_lt).ne'
+  exact (Nat.one_lt_pow k.succ_ne_zero hp.out.one_lt).ne'
 #align range_pow_padic_val_nat_subset_divisors' range_pow_padicValNat_subset_divisors'
 
 /-- The `p`-adic valuation of `(p * n)!` is `n` more than that of `n!`. -/
diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean
index 6cb099bda9605..adbf68fda317d 100644
--- a/Mathlib/NumberTheory/Padics/RingHoms.lean
+++ b/Mathlib/NumberTheory/Padics/RingHoms.lean
@@ -533,7 +533,7 @@ theorem nthHomSeq_one : nthHomSeq f_compat 1 ≈ 1 := by
   change _ < _ at hε
   use 1
   intro j hj
-  haveI : Fact (1 < p ^ j) := ⟨Nat.one_lt_pow _ _ (by omega) hp_prime.1.one_lt⟩
+  haveI : Fact (1 < p ^ j) := ⟨Nat.one_lt_pow (by omega) hp_prime.1.one_lt⟩
   suffices (ZMod.cast (1 : ZMod (p ^ j)) : ℚ) = 1 by simp [nthHomSeq, nthHom, this, hε]
   rw [ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one]
 #align padic_int.nth_hom_seq_one PadicInt.nthHomSeq_one
diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean
index bca9e21fbb955..affe41238025d 100644
--- a/Mathlib/NumberTheory/PellMatiyasevic.lean
+++ b/Mathlib/NumberTheory/PellMatiyasevic.lean
@@ -250,7 +250,7 @@ theorem pell_eq (n : ℕ) : xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n = 1 :=
 instance dnsq : Zsqrtd.Nonsquare (d a1) :=
   ⟨fun n h =>
     have : n * n + 1 = a * a := by rw [← h]; exact Nat.succ_pred_eq_of_pos (asq_pos a1)
-    have na : n < a := Nat.mul_self_lt_mul_self_iff.2 (by rw [← this]; exact Nat.lt_succ_self _)
+    have na : n < a := Nat.mul_self_lt_mul_self_iff.1 (by rw [← this]; exact Nat.lt_succ_self _)
     have : (n + 1) * (n + 1) ≤ n * n + 1 := by rw [this]; exact Nat.mul_self_le_mul_self na
     have : n + n ≤ 0 :=
       @Nat.le_of_add_le_add_right _ (n * n + 1) _ (by ring_nf at this ⊢; assumption)
diff --git a/Mathlib/NumberTheory/Zsqrtd/Basic.lean b/Mathlib/NumberTheory/Zsqrtd/Basic.lean
index fd014b2ec79b4..e3de7c00f64a3 100644
--- a/Mathlib/NumberTheory/Zsqrtd/Basic.lean
+++ b/Mathlib/NumberTheory/Zsqrtd/Basic.lean
@@ -433,7 +433,7 @@ theorem sqLe_of_le {c d x y z w : ℕ} (xz : z ≤ x) (yw : y ≤ w) (xy : SqLe
 
 theorem sqLe_add_mixed {c d x y z w : ℕ} (xy : SqLe x c y d) (zw : SqLe z c w d) :
     c * (x * z) ≤ d * (y * w) :=
-  Nat.mul_self_le_mul_self_iff.2 <| by
+  Nat.mul_self_le_mul_self_iff.1 <| by
     simpa [mul_comm, mul_left_comm] using mul_le_mul xy zw (Nat.zero_le _) (Nat.zero_le _)
 #align zsqrtd.sq_le_add_mixed Zsqrtd.sqLe_add_mixed
 
@@ -681,7 +681,7 @@ theorem nonneg_add_lem {x y z w : ℕ} (xy : Nonneg (⟨x, -y⟩ : ℤ√d)) (zw
           (fun m n xy zw => sqLe_cancel xy zw) fun m n xy zw =>
           let t := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
           have : k + j + 1 ≤ k :=
-            Nat.mul_self_le_mul_self_iff.2 (by simpa [one_mul] using t)
+            Nat.mul_self_le_mul_self_iff.1 (by simpa [one_mul] using t)
           absurd this (not_le_of_gt <| Nat.succ_le_succ <| Nat.le_add_right _ _))
       (nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw)
   rw [add_def, neg_add_eq_sub]
diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean
index 3a74b8e65e209..9d26db0640a32 100644
--- a/Mathlib/RingTheory/Multiplicity.lean
+++ b/Mathlib/RingTheory/Multiplicity.lean
@@ -8,7 +8,6 @@ import Mathlib.Algebra.Associated
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Data.Nat.PartENat
 import Mathlib.Tactic.Linarith
-import Mathlib.Data.Nat.Pow
 
 #align_import ring_theory.multiplicity from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 
diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean
index 7c0b1003114d5..aa65943f485ed 100644
--- a/Mathlib/Tactic/Positivity/Basic.lean
+++ b/Mathlib/Tactic/Positivity/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mario Carneiro, Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Heather Macbeth, Yaël Dillies
 -/
+import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Data.Int.CharZero
 import Mathlib.Data.Int.Order.Basic
 import Mathlib.Data.Nat.Factorial.Basic
diff --git a/scripts/noshake.json b/scripts/noshake.json
index 36816dec9d72c..aef27127fac54 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -221,7 +221,9 @@
   "Mathlib.Tactic.ProdAssoc": ["Mathlib.Logic.Equiv.Defs"],
   "Mathlib.Tactic.Positivity.Finset": ["Mathlib.Data.Fintype.Card"],
   "Mathlib.Tactic.Positivity.Basic":
-  ["Mathlib.Data.Int.CharZero", "Mathlib.Data.Nat.Factorial.Basic"],
+  ["Mathlib.Algebra.GroupPower.Order",
+   "Mathlib.Data.Int.CharZero",
+   "Mathlib.Data.Nat.Factorial.Basic"],
   "Mathlib.Tactic.NormNum.Ineq":
   ["Mathlib.Algebra.Order.Field.Defs", "Mathlib.Algebra.Order.Monoid.WithTop"],
   "Mathlib.Tactic.NormNum.BigOperators": ["Mathlib.Data.List.FinRange"],
@@ -339,4 +341,4 @@
   "Mathlib.Algebra.Category.Ring.Basic":
   ["Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso"],
   "Mathlib.Algebra.Algebra.Subalgebra.Order":
-  ["Mathlib.Algebra.Module.Submodule.Order"]}}
\ No newline at end of file
+  ["Mathlib.Algebra.Module.Submodule.Order"]}}