chore: delay imports of OrderedRing via PNat (#14182)

Mathlib.lean

@@ -2227,6 +2227,7 @@ import Mathlib.Data.PFunctor.Univariate.Basic
 import Mathlib.Data.PFunctor.Univariate.M
 import Mathlib.Data.PNat.Basic
 import Mathlib.Data.PNat.Defs
+import Mathlib.Data.PNat.Equiv
 import Mathlib.Data.PNat.Factors
 import Mathlib.Data.PNat.Find
 import Mathlib.Data.PNat.Interval

Mathlib/Computability/Primrec.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Logic.Equiv.List
 import Mathlib.Logic.Function.Iterate
+import Mathlib.Algebra.Order.Ring.Nat
 
 #align_import computability.primrec from "leanprover-community/mathlib"@"2738d2ca56cbc63be80c3bd48e9ed90ad94e947d"
 

Mathlib/Data/PNat/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Ralf Stephan, Neil Strickland, Ruben Van de Velde
 -/
-import Mathlib.Data.PNat.Defs
+import Mathlib.Data.PNat.Equiv
 import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Set.Basic
 import Mathlib.Algebra.GroupWithZero.Divisibility
@@ -148,17 +148,6 @@ instance contravariantClass_add_le : ContravariantClass ℕ+ ℕ+ (· + ·) (·
 instance contravariantClass_add_lt : ContravariantClass ℕ+ ℕ+ (· + ·) (· < ·) :=
   Positive.contravariantClass_add_lt
 
-/-- An equivalence between `ℕ+` and `ℕ` given by `PNat.natPred` and `Nat.succPNat`. -/
-@[simps (config := .asFn)]
-def _root_.Equiv.pnatEquivNat : ℕ+ ≃ ℕ where
-  toFun := PNat.natPred
-  invFun := Nat.succPNat
-  left_inv := succPNat_natPred
-  right_inv := Nat.natPred_succPNat
-#align equiv.pnat_equiv_nat Equiv.pnatEquivNat
-#align equiv.pnat_equiv_nat_symm_apply Equiv.pnatEquivNat_symm_apply
-#align equiv.pnat_equiv_nat_apply Equiv.pnatEquivNat_apply
-
 /-- The order isomorphism between ℕ and ℕ+ given by `succ`. -/
 @[simps! (config := .asFn) apply]
 def _root_.OrderIso.pnatIsoNat : ℕ+ ≃o ℕ where

Mathlib/Data/PNat/Equiv.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Ralf Stephan, Neil Strickland, Ruben Van de Velde
+-/
+import Mathlib.Data.PNat.Defs
+import Mathlib.Logic.Equiv.Defs
+
+/-!
+# The equivalence between `ℕ+` and `ℕ`
+-/
+
+/-- An equivalence between `ℕ+` and `ℕ` given by `PNat.natPred` and `Nat.succPNat`. -/
+@[simps (config := .asFn)]
+def _root_.Equiv.pnatEquivNat : ℕ+ ≃ ℕ where
+  toFun := PNat.natPred
+  invFun := Nat.succPNat
+  left_inv := PNat.succPNat_natPred
+  right_inv := Nat.natPred_succPNat
+#align equiv.pnat_equiv_nat Equiv.pnatEquivNat
+#align equiv.pnat_equiv_nat_symm_apply Equiv.pnatEquivNat_symm_apply
+#align equiv.pnat_equiv_nat_apply Equiv.pnatEquivNat_apply

Mathlib/Data/W/Basic.lean

@@ -167,7 +167,7 @@ private def f (n : ℕ) : WType' β (n + 1) → Σa : α, β a → WType' β n
 private def finv (n : ℕ) : (Σa : α, β a → WType' β n) → WType' β (n + 1)
   | ⟨a, f⟩ =>
     let f' := fun i : β a => (f i).val
-    have : WType.depth ⟨a, f'⟩ ≤ n + 1 := add_le_add_right (Finset.sup_le fun b _ => (f b).2) 1
+    have : WType.depth ⟨a, f'⟩ ≤ n + 1 := Nat.add_le_add_right (Finset.sup_le fun b _ => (f b).2) 1
     ⟨⟨a, f'⟩, this⟩
 
 variable [Encodable α]

Mathlib/Logic/Denumerable.lean

@@ -23,6 +23,7 @@ This property already has a name, namely `α ≃ ℕ`, but here we are intereste
 typeclass.
 -/
 
+assert_not_exists OrderedSemiring
 
 variable {α β : Type*}
 
@@ -144,7 +145,7 @@ instance sum : Denumerable (Sum α β) :=
     suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_decomp]
     simp only [decodeSum, boddDiv2_eq, decode_eq_ofNat, Option.some.injEq, Option.map_some',
       Option.mem_def, Sum.exists]
-    cases bodd n <;> simp [decodeSum, bit, encodeSum, bit0_eq_two_mul, bit1]⟩
+    cases bodd n <;> simp [decodeSum, bit, encodeSum, bit0, bit1, Nat.two_mul]⟩
 #align denumerable.sum Denumerable.sum
 
 section Sigma
@@ -221,7 +222,7 @@ open scoped Classical
 theorem exists_succ (x : s) : ∃ n, (x : ℕ) + n + 1 ∈ s :=
   _root_.by_contradiction fun h =>
     have : ∀ (a : ℕ) (_ : a ∈ s), a < x + 1 := fun a ha =>
-      lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [add_right_comm, add_tsub_cancel_of_le hax]⟩
+      lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [add_right_comm, Nat.add_sub_cancel' hax]⟩
     Fintype.false
       ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
             (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy)
@@ -243,25 +244,21 @@ theorem succ_le_of_lt {x y : s} (h : y < x) : succ y ≤ x :=
   have hx : ∃ m, (y : ℕ) + m + 1 ∈ s := exists_succ _
   let ⟨k, hk⟩ := Nat.exists_eq_add_of_lt h
   have : Nat.find hx ≤ k := Nat.find_min' _ (hk ▸ x.2)
-  show (y : ℕ) + Nat.find hx + 1 ≤ x by
-    rw [hk]
-    exact add_le_add_right (add_le_add_left this _) _
+  show (y : ℕ) + Nat.find hx + 1 ≤ x by omega
 #align nat.subtype.succ_le_of_lt Nat.Subtype.succ_le_of_lt
 
 theorem le_succ_of_forall_lt_le {x y : s} (h : ∀ z < x, z ≤ y) : x ≤ succ y :=
   have hx : ∃ m, (y : ℕ) + m + 1 ∈ s := exists_succ _
   show (x : ℕ) ≤ (y : ℕ) + Nat.find hx + 1 from
     le_of_not_gt fun hxy =>
       (h ⟨_, Nat.find_spec hx⟩ hxy).not_lt <|
-        calc
-          (y : ℕ) ≤ (y : ℕ) + Nat.find hx := le_add_of_nonneg_right (Nat.zero_le _)
-          _ < (y : ℕ) + Nat.find hx + 1 := Nat.lt_succ_self _
+        (by omega : (y : ℕ) < (y : ℕ) + Nat.find hx + 1)
 #align nat.subtype.le_succ_of_forall_lt_le Nat.Subtype.le_succ_of_forall_lt_le
 
 theorem lt_succ_self (x : s) : x < succ x :=
   calc
     -- Porting note: replaced `x + _`, added type annotations
-    (x : ℕ) ≤ (x + Nat.find (exists_succ x): ℕ) := le_self_add
+    (x : ℕ) ≤ (x + Nat.find (exists_succ x) : ℕ) := le_add_right ..
     _ < (succ x : ℕ) := Nat.lt_succ_self (x + _)
 #align nat.subtype.lt_succ_self Nat.Subtype.lt_succ_self
 

Mathlib/Logic/Encodable/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Mathlib.Logic.Equiv.Nat
-import Mathlib.Data.PNat.Basic
+import Mathlib.Data.PNat.Equiv
 import Mathlib.Order.Directed
 import Mathlib.Data.Countable.Defs
 import Mathlib.Order.RelIso.Basic
@@ -36,7 +36,6 @@ The point of asking for an explicit partial inverse `decode : ℕ → Option α`
 to make the range of `encode` decidable even when the finiteness of `α` is not.
 -/
 
-
 open Option List Nat Function
 
 /-- Constructively countable type. Made from an explicit injection `encode : α → ℕ` and a partial

Mathlib/Logic/Equiv/List.lean

@@ -299,14 +299,14 @@ def raise : List ℕ → ℕ → List ℕ
 
 theorem lower_raise : ∀ l n, lower (raise l n) n = l
   | [], n => rfl
-  | m :: l, n => by rw [raise, lower, add_tsub_cancel_right, lower_raise l]
+  | m :: l, n => by rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]
 #align denumerable.lower_raise Denumerable.lower_raise
 
 theorem raise_lower : ∀ {l n}, List.Sorted (· ≤ ·) (n :: l) → raise (lower l n) n = l
   | [], n, _ => rfl
   | m :: l, n, h => by
     have : n ≤ m := List.rel_of_sorted_cons h _ (l.mem_cons_self _)
-    simp [raise, lower, tsub_add_cancel_of_le this, raise_lower h.of_cons]
+    simp [raise, lower, Nat.sub_add_cancel this, raise_lower h.of_cons]
 #align denumerable.raise_lower Denumerable.raise_lower
 
 theorem raise_chain : ∀ l n, List.Chain (· ≤ ·) n (raise l n)
@@ -363,7 +363,7 @@ theorem raise_lower' : ∀ {l n}, (∀ m ∈ l, n ≤ m) → List.Sorted (· < 
   | [], n, _, _ => rfl
   | m :: l, n, h₁, h₂ => by
     have : n ≤ m := h₁ _ (l.mem_cons_self _)
-    simp [raise', lower', tsub_add_cancel_of_le this,
+    simp [raise', lower', Nat.sub_add_cancel this,
       raise_lower' (List.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) h₂.of_cons]
 #align denumerable.raise_lower' Denumerable.raise_lower'
 

Mathlib/ModelTheory/Ultraproducts.lean

@@ -24,7 +24,6 @@ ultraproduct, Los's theorem
 
 -/
 
-
 universe u v
 
 variable {α : Type*} (M : α → Type*) (u : Ultrafilter α)

Mathlib/Order/Filter/AtTopBot.lean

@@ -13,6 +13,7 @@ import Mathlib.Order.Interval.Set.Disjoint
 import Mathlib.Order.Interval.Set.OrderIso
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.Filter.Bases
+import Mathlib.Algebra.Order.Ring.Nat
 
 #align_import order.filter.at_top_bot from "leanprover-community/mathlib"@"1f0096e6caa61e9c849ec2adbd227e960e9dff58"
 

Mathlib/Order/OrderIsoNat.lean

@@ -69,7 +69,7 @@ theorem acc_iff_no_decreasing_seq {x} :
   · refine fun h => h.recOn fun x _ IH => ?_
     constructor
     rintro ⟨f, k, hf⟩
-    exact IsEmpty.elim' (IH (f (k + 1)) (hf ▸ f.map_rel_iff.2 (lt_add_one k))) ⟨f, _, rfl⟩
+    exact IsEmpty.elim' (IH (f (k + 1)) (hf ▸ f.map_rel_iff.2 (Nat.lt_succ_self _))) ⟨f, _, rfl⟩
   · have : ∀ x : { a // ¬Acc r a }, ∃ y : { a // ¬Acc r a }, r y.1 x.1 := by
       rintro ⟨x, hx⟩
       cases exists_not_acc_lt_of_not_acc hx with
@@ -185,13 +185,12 @@ theorem exists_increasing_or_nonincreasing_subseq' (r : α → α → Prop) (f :
         · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
       have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
         intro n
-        have h := hm _ (le_add_of_nonneg_left n.zero_le)
+        have h := hm _ (Nat.le_add_left m n)
         simp only [bad, exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
         obtain ⟨n', hn1, hn2⟩ := h
-        obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1
-        refine ⟨n + x, add_lt_add_left hpos n, ?_⟩
-        rw [add_assoc, add_comm x m, ← add_assoc]
-        exact hn2
+        refine ⟨n + n' - n - m, by omega, ?_⟩
+        convert hn2
+        omega
       let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
       exact
         ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
@@ -206,7 +205,7 @@ theorem exists_increasing_or_nonincreasing_subseq (r : α → α → Prop) [IsTr
       (∀ m n : ℕ, m < n → r (f (g m)) (f (g n))) ∨ ∀ m n : ℕ, m < n → ¬r (f (g m)) (f (g n)) := by
   obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
   · refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
-    obtain ⟨x, rfl⟩ := exists_add_of_le (Nat.succ_le_iff.2 mn)
+    obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)
     induction' x with x ih
     · apply hr
     · apply IsTrans.trans _ _ _ _ (hr _)

Mathlib/Order/SuccPred/LinearLocallyFinite.lean

@@ -7,6 +7,7 @@ import Mathlib.Data.Countable.Basic
 import Mathlib.Logic.Encodable.Basic
 import Mathlib.Order.SuccPred.Basic
 import Mathlib.Order.Interval.Finset.Defs
+import Mathlib.Algebra.Order.Ring.Nat
 
 #align_import order.succ_pred.linear_locally_finite from "leanprover-community/mathlib"@"2705404e701abc6b3127da906f40bae062a169c9"
 

Mathlib/Order/WellFoundedSet.lean

@@ -47,6 +47,7 @@ Prove that `s` is partial well ordered iff it has no infinite descending chain o
  * [Nash-Williams, *On Well-Quasi-Ordering Finite Trees*][Nash-Williams63]
 -/
 
+assert_not_exists OrderedSemiring
 
 variable {ι α β γ : Type*} {π : ι → Type*}
 
@@ -392,7 +393,7 @@ theorem partiallyWellOrderedOn_iff_exists_monotone_subseq :
   constructor <;> intro h f hf
   · exact h.exists_monotone_subseq f hf
   · obtain ⟨g, gmon⟩ := h f hf
-    exact ⟨g 0, g 1, g.lt_iff_lt.2 zero_lt_one, gmon _ _ zero_le_one⟩
+    exact ⟨g 0, g 1, g.lt_iff_lt.2 Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩
 #align set.partially_well_ordered_on_iff_exists_monotone_subseq Set.partiallyWellOrderedOn_iff_exists_monotone_subseq
 
 protected theorem PartiallyWellOrderedOn.prod {t : Set β} (hs : PartiallyWellOrderedOn s r)
@@ -554,7 +555,7 @@ protected theorem IsWF.isPWO (hs : s.IsWF) : s.IsPWO := by
   lift f to ℕ → s using hf
   rcases hs.has_min (range f) (range_nonempty _) with ⟨_, ⟨m, rfl⟩, hm⟩
   simp only [forall_mem_range, not_lt] at hm
-  exact ⟨m, m + 1, lt_add_one m, hm _⟩
+  exact ⟨m, m + 1, by omega, hm _⟩
 #align set.is_wf.is_pwo Set.IsWF.isPWO
 
 /-- In a linear order, the predicates `Set.IsWF` and `Set.IsPWO` are equivalent. -/
@@ -712,7 +713,8 @@ theorem BddBelow.wellFoundedOn_lt : BddBelow s → s.WellFoundedOn (· < ·) :=
   rintro ⟨a, ha⟩ f hf
   refine infinite_range_of_injective f.injective ?_
   exact (finite_Icc a <| f 0).subset <| range_subset_iff.2 <| fun n =>
-    ⟨ha <| hf _, antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| zero_le _⟩
+    ⟨ha <| hf _,
+      antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| Nat.zero_le _⟩
 
 theorem BddAbove.wellFoundedOn_gt : BddAbove s → s.WellFoundedOn (· > ·) :=
   fun h => h.dual.wellFoundedOn_lt
@@ -765,7 +767,7 @@ theorem exists_min_bad_of_exists_bad (r : α → α → Prop) (rk : α → ℕ)
     · exact ⟨(minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).1,
         (minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).2.2⟩
   have h : ∀ m n, m ≤ n → (fs m).1 m = (fs n).1 m := fun m n mn => by
-    obtain ⟨k, rfl⟩ := exists_add_of_le mn; clear mn
+    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le mn; clear mn
     induction' k with k ih
     · rfl
     · rw [ih, (minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
@@ -809,7 +811,7 @@ theorem partiallyWellOrderedOn_sublistForall₂ (r : α → α → Prop) [IsRefl
     hf2 (g 0) (fun n => if n < g 0 then f n else List.tail (f (g (n - g 0))))
       (fun m hm => (if_pos hm).symm) ?_
   swap;
-  · simp only [if_neg (lt_irrefl (g 0)), tsub_self]
+  · simp only [if_neg (lt_irrefl (g 0)), Nat.sub_self]
     rw [List.length_tail, ← Nat.pred_eq_sub_one]
     exact Nat.pred_lt fun con => hnil _ (List.length_eq_zero.1 con)
   rw [IsBadSeq] at hf'
@@ -820,12 +822,12 @@ theorem partiallyWellOrderedOn_sublistForall₂ (r : α → α → Prop) [IsRefl
   by_cases hn : n < g 0
   · apply hf1.2 m n mn
     rwa [if_pos hn, if_pos (mn.trans hn)] at hmn
-  · obtain ⟨n', rfl⟩ := exists_add_of_le (not_lt.1 hn)
-    rw [if_neg hn, add_comm (g 0) n', add_tsub_cancel_right] at hmn
+  · obtain ⟨n', rfl⟩ := Nat.exists_eq_add_of_le (not_lt.1 hn)
+    rw [if_neg hn, add_comm (g 0) n', Nat.add_sub_cancel_right] at hmn
     split_ifs at hmn with hm
     · apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))
       exact _root_.trans hmn (List.tail_sublistForall₂_self _)
-    · rw [← tsub_lt_iff_left (le_of_not_lt hm)] at mn
+    · rw [← Nat.sub_lt_iff_lt_add (le_of_not_lt hm)] at mn
       apply hf1.2 _ _ (g.lt_iff_lt.2 mn)
       rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g n'))]
       exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn
@@ -862,7 +864,7 @@ theorem subsetProdLex [PartialOrder α] [Preorder β] {s : Set (α ×ₗ β)}
       right
       constructor
       · exact (hhc (g' 0)).symm.trans (hhc (g' 1))
-      · exact hg' zero_le_one
+      · exact hg' (Nat.zero_le 1)
 
 theorem imageProdLex [PartialOrder α] [Preorder β] {s : Set (α ×ₗ β)}
     (hαβ : s.IsPWO) : ((fun (x : α ×ₗ β) => (ofLex x).1)'' s).IsPWO :=

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Floris van Doorn, Violeta Hernández Palacios
 -/
 import Mathlib.SetTheory.Ordinal.Basic
 import Mathlib.Data.Nat.SuccPred
+import Mathlib.Algebra.GroupWithZero.Divisibility
 
 #align_import set_theory.ordinal.arithmetic from "leanprover-community/mathlib"@"31b269b60935483943542d547a6dd83a66b37dc7"
 

Mathlib/SetTheory/Ordinal/Notation.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Init.Data.Ordering.Lemmas
 import Mathlib.SetTheory.Ordinal.Principal
 import Mathlib.Tactic.NormNum
+import Mathlib.Data.PNat.Basic
 
 #align_import set_theory.ordinal.notation from "leanprover-community/mathlib"@"b67044ba53af18680e1dd246861d9584e968495d"