chore: deprecate duplicate theorems on ENat (#39854)

vihdzp · vihdzp · commit 4b5956c179b8 · 2026-05-27T17:34:23.000Z
These exist more generally in the setting of `SuccAddOrder`.
diff --git a/Mathlib/Algebra/Order/SuccPred.lean b/Mathlib/Algebra/Order/SuccPred.lean
@@ -241,34 +241,36 @@ theorem add_one_inj [NoMaxOrder α] : x + 1 = y + 1 ↔ x = y := by
 
 end Add
 
+@[simp]
+theorem lt_two_iff [AddMonoidWithOne α] [SuccAddOrder α] [NoMaxOrder α] : x < 2 ↔ x ≤ 1 := by
+  rw [← one_add_one_eq_two, lt_add_one_iff]
+
 section AddMonoidWithOne
-variable [AddMonoidWithOne α] [NoMaxOrder α] [SuccAddOrder α]
+variable [AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α] [NeZero (1 : α)]
 
 @[simp]
-theorem lt_one_iff [IsBotZeroClass α] : x < 1 ↔ x = 0 := by
-  rw [← zero_add 1, lt_add_one_iff, nonpos_iff_eq_zero]
+theorem lt_one_iff : x < 1 ↔ x = 0 := by
+  simpa using (one_le_iff_ne_zero (x := x)).not
 
-theorem le_one_iff [IsBotZeroClass α] : x ≤ 1 ↔ x = 0 ∨ x = 1 := by
+theorem le_one_iff : x ≤ 1 ↔ x = 0 ∨ x = 1 := by
   rw [le_iff_lt_or_eq, lt_one_iff]
 
 @[simp]
-theorem Iio_one [IsBotZeroClass α] : Set.Iio (1 : α) = {0} := by
+theorem Iio_one : Set.Iio (1 : α) = {0} := by
   ext; simp
 
-theorem Iic_one [IsBotZeroClass α] : Set.Iic (1 : α) = {0, 1} := by
+theorem Iic_one : Set.Iic (1 : α) = {0, 1} := by
   ext; simp [le_one_iff]
 
-@[simp]
-theorem lt_two_iff : x < 2 ↔ x ≤ 1 := by
-  rw [← one_add_one_eq_two, lt_add_one_iff]
+variable [NoMaxOrder α]
 
-theorem le_two_iff [IsBotZeroClass α] : x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2 := by
+theorem le_two_iff : x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2 := by
   rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]
 
-theorem Iio_two [IsBotZeroClass α] : Set.Iio (2 : α) = {0, 1} := by
+theorem Iio_two : Set.Iio (2 : α) = {0, 1} := by
   ext; simp [le_one_iff]
 
-theorem Iic_two [IsBotZeroClass α] : Set.Iic (2 : α) = {0, 1, 2} := by
+theorem Iic_two : Set.Iic (2 : α) = {0, 1, 2} := by
   ext; simp [le_two_iff]
 
 end AddMonoidWithOne
diff --git a/Mathlib/Analysis/Analytic/Order.lean b/Mathlib/Analysis/Analytic/Order.lean
@@ -298,8 +298,8 @@ theorem AnalyticAt.analyticOrderAt_deriv_add_one {x : 𝕜} (hf : AnalyticAt 
       · simp_rw [← Nat.cast_smul_eq_nsmul 𝕜]
         fun_prop
     rwa [← Pi.add_def, analyticOrderAt_add_eq_right_of_lt]
-    rw [this, ← Order.succ_le_iff_of_not_isMax (not_isMax_iff.mpr ⟨⊤, ENat.coe_lt_top s⟩),
-      ENat.succ_def, ← Nat.cast_add_one, natCast_le_analyticOrderAt (by fun_prop)]
+    rw [this, ← ENat.add_one_le_iff (ENat.coe_ne_top _), ← Nat.cast_add_one,
+      natCast_le_analyticOrderAt (by fun_prop)]
     exact ⟨deriv F, hFa.deriv, by simp⟩
 
 theorem AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero {x : 𝕜} (hf : AnalyticAt 𝕜 f x)
diff --git a/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean b/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
@@ -381,14 +381,14 @@ noncomputable def fderivLM :
     else 0
   map_add' f g := by
     split_ifs with hk
-    · have hk' : 0 < (n : ℕ∞ω) := mod_cast (ENat.add_one_pos.trans_le hk)
+    · have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk
       ext
       simp [fderiv_add (f.contDiff.differentiable hk'.ne').differentiableAt
                        (g.contDiff.differentiable hk'.ne').differentiableAt]
     · simp
   map_smul' c f := by
     split_ifs with hk
-    · have hk' : 0 < (n : ℕ∞ω) := mod_cast (ENat.add_one_pos.trans_le hk)
+    · have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk
       ext
       simp [fderiv_const_smul (f.contDiff.differentiable hk'.ne').differentiableAt]
     · simp
diff --git a/Mathlib/Analysis/Distribution/TestFunction.lean b/Mathlib/Analysis/Distribution/TestFunction.lean
@@ -567,7 +567,7 @@ lemma lineDerivCLM_apply {f : 𝓓^{n}(Ω, F)} {v : E} {x : E} :
     (lineDerivCLM 𝕜 v f : 𝓓^{k}(Ω, F)) x = if k + 1 ≤ n then lineDeriv ℝ f x v else 0 := by
   rw [lineDerivCLM_eq_fderivCLM, fderivCLM_apply]
   split_ifs with hk
-  · have hk' : 0 < (n : ℕ∞ω) := mod_cast (ENat.add_one_pos.trans_le hk)
+  · have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk
     rw [(f.contDiff.differentiable hk'.ne').differentiableAt.lineDeriv_eq_fderiv]
   · rfl
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean
@@ -68,7 +68,7 @@ protected lemma IsEdgeReachable.zero : G.IsEdgeReachable 0 u v := by simp [IsEdg
 
 @[simp]
 lemma isEdgeReachable_one : G.IsEdgeReachable 1 u v ↔ G.Reachable u v := by
-  simp [IsEdgeReachable, ENat.lt_one_iff_eq_zero]
+  simp [IsEdgeReachable, Order.lt_one_iff]
 
 @[simp]
 lemma isEdgeConnected_one : G.IsEdgeConnected 1 ↔ G.Preconnected := by
diff --git a/Mathlib/Combinatorics/SimpleGraph/Diam.lean b/Mathlib/Combinatorics/SimpleGraph/Diam.lean
@@ -114,7 +114,7 @@ lemma eccent_le_one_iff (u : α) : G.eccent u ≤ 1 ↔ ∀ v, u ≠ v → G.Adj
 
 lemma eccent_eq_one_iff [Nontrivial α] (u : α) :
     G.eccent u = 1 ↔ ∀ v, u ≠ v → G.Adj u v := by
-  have h : 1 ≤ G.eccent u := ENat.one_le_iff_ne_zero.mpr (eccent_ne_zero u)
+  have h : 1 ≤ G.eccent u := Order.one_le_iff_ne_zero.mpr (eccent_ne_zero u)
   rw [← h.ge_iff_eq']
   exact eccent_le_one_iff u
 
@@ -368,9 +368,9 @@ lemma radius_ne_top_iff [Nonempty α] [Finite α] : G.radius ≠ ⊤ ↔ G.Conne
   exact h u v
 
 lemma radius_ne_zero_of_nontrivial [Nontrivial α] : G.radius ≠ 0 := by
-  rw [← ENat.one_le_iff_ne_zero]
+  rw [← Order.one_le_iff_ne_zero]
   apply le_iInf
-  simp [ENat.one_le_iff_ne_zero, G.eccent_ne_zero]
+  simp [Order.one_le_iff_ne_zero, G.eccent_ne_zero]
 
 lemma radius_eq_zero_iff : G.radius = 0 ↔ Nonempty α ∧ Subsingleton α := by
   refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨_, _⟩ ↦ ?_⟩
diff --git a/Mathlib/Combinatorics/SimpleGraph/Metric.lean b/Mathlib/Combinatorics/SimpleGraph/Metric.lean
@@ -157,8 +157,8 @@ lemma edist_eq_two_iff {u v : V} :
     rw [mem_commonNeighbors] at hw
     have := (Walk.cons hw.1 <| .cons hw.2.symm .nil).edist_le
     simp_all
-  · by_contra! hc
-    cases ENat.le_one_iff_eq_zero_or_eq_one.mp (Order.le_of_lt_succ hc) <;> simp_all
+  · by_contra
+    simp_all [Order.le_one_iff]
 
 lemma two_lt_edist_iff {u v : V} :
     2 < G.edist u v ↔ u ≠ v ∧ ¬ G.Adj u v ∧ (G.commonNeighbors u v) = ∅ := by
@@ -418,7 +418,7 @@ theorem ball_zero : G.ball c 0 = ∅ := by simp [ball]
 /-- The ball of radius one consists of just the center. -/
 @[simp]
 theorem ball_one : G.ball c 1 = {c} := by
-  simp [ball, ENat.lt_one_iff_eq_zero]
+  simp [ball]
 
 /-- The ball of radius two consists of the center and its neighbors. -/
 @[simp]
diff --git a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
@@ -74,14 +74,10 @@ theorem IsSRGWith.ediam_eq_two [Nontrivial V] (h : G.IsSRGWith n k ℓ μ) (ht :
     by_contra! hc
     obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc
     have h := h.of_not_adj hn ha
-    simp_rw [he, Fintype.card_eq_zero] at h
-    exact false_of_ne (h ▸ hm)
-  · by_contra! hc
-    cases ENat.le_one_iff_eq_zero_or_eq_one.mp (Order.le_of_lt_succ hc) with
-    | inl hc =>
-      rw [ediam_eq_zero_iff_subsingleton] at hc
-      exact false_of_nontrivial_of_subsingleton V
-    | inr hc => exact ht.elim (ediam_eq_one.mp hc)
+    simp_all
+  · by_contra
+    have := not_subsingleton V
+    simp_all [Order.le_one_iff]
 
 /-- **Conway's 99-graph problem** (from https://oeis.org/A248380/a248380.pdf)
 can be reformulated as the existence of a strongly regular graph with params (99, 14, 1, 2).
diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
@@ -126,9 +126,8 @@ def lift (x : ℕ∞) (h : x < ⊤) : ℕ := WithTop.untop x (WithTop.lt_top_iff
 
 instance canLift : CanLift ℕ∞ ℕ (↑) (· ≠ ⊤) := WithTop.canLift
 
-instance : WellFoundedRelation ℕ∞ where
-  rel := (· < ·)
-  wf := IsWellFounded.wf
+instance : WellFoundedRelation ℕ∞ :=
+  WellFoundedLT.toWellFoundedRelation
 
 /-- Conversion of `ℕ∞` to `ℕ` sending `∞` to `0`. -/
 def toNat : ℕ∞ → ℕ := WithTop.untopD 0
@@ -272,7 +271,7 @@ lemma toNat_le_of_le_coe {m : ℕ∞} {n : ℕ} (h : m ≤ n) : toNat m ≤ n :=
 lemma toNat_le_toNat {m n : ℕ∞} (h : m ≤ n) (hn : n ≠ ⊤) : toNat m ≤ toNat n :=
   toNat_le_of_le_coe <| h.trans_eq (coe_toNat hn).symm
 
--- TODO: deprecate
+@[deprecated Order.succ_eq_add_one (since := "2026-05-25")]
 theorem succ_def (m : ℕ∞) : Order.succ m = m + 1 :=
   Order.succ_eq_add_one m
 
@@ -284,21 +283,25 @@ theorem add_one_le_iff' (hn : n ≠ ⊤) : m + 1 ≤ n ↔ m < n := by
   · simpa
   · exact add_one_le_iff hm
 
-theorem one_le_iff_ne_zero : 1 ≤ n ↔ n ≠ 0 :=
-  Order.one_le_iff_pos.trans pos_iff_ne_zero
+@[deprecated Order.one_le_iff_ne_zero (since := "2026-05-25")]
+protected theorem one_le_iff_ne_zero : 1 ≤ n ↔ n ≠ 0 :=
+  Order.one_le_iff_ne_zero
 
+@[deprecated Order.lt_one_iff (since := "2026-05-25")]
 lemma lt_one_iff_eq_zero : n < 1 ↔ n = 0 :=
-  not_le.symm.trans one_le_iff_ne_zero.not_left
+  Order.lt_one_iff
 
-lemma le_one_iff_eq_zero_or_eq_one : n ≤ 1 ↔ n = 0 ∨ n = 1 := by
-  refine ⟨fun h ↦ ?_, fun h ↦ by cases h <;> simp_all⟩
-  cases n
-  · simp at h
-  · rwa [← lt_one_iff_eq_zero, ← le_iff_lt_or_eq]
+@[deprecated Order.le_one_iff (since := "2026-05-25")]
+lemma le_one_iff_eq_zero_or_eq_one : n ≤ 1 ↔ n = 0 ∨ n = 1 :=
+  Order.le_one_iff
 
 theorem lt_add_one_iff (hm : n ≠ ⊤) : m < n + 1 ↔ m ≤ n :=
   Order.lt_add_one_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)
 
+@[simp]
+theorem lt_two_iff : n < 2 ↔ n ≤ 1 := by
+  rw [← one_add_one_eq_two, lt_add_one_iff one_ne_top]
+
 theorem add_le_add_iff_left {m n k : ENat} (h : k ≠ ⊤) :
     k + n ≤ k + m ↔ n ≤ m :=
   WithTop.add_le_add_iff_left h
@@ -337,8 +340,9 @@ theorem nat_induction {motive : ℕ∞ → Prop} (a : ℕ∞) (zero : motive 0)
   · exact top A
   · exact A _
 
+@[deprecated add_pos_of_right (since := "2026-05-25")]
 lemma add_one_pos : 0 < n + 1 :=
-  succ_def n ▸ Order.bot_lt_succ n
+  add_pos_of_right zero_lt_one n
 
 lemma natCast_lt_succ {n : ℕ} :
     (n : ℕ∞) < (n : ℕ∞) + 1 := by
@@ -438,7 +442,7 @@ lemma self_le_mul_right (a : ℕ∞) (hc : c ≠ 0) : a ≤ a * c := by
   · simp [top_mul hc]
   obtain rfl | h0 := eq_or_ne a 0
   · simp
-  nth_rewrite 1 [← mul_one a, ENat.mul_le_mul_left_iff h0 hne, ENat.one_le_iff_ne_zero]
+  nth_rewrite 1 [← mul_one a, ENat.mul_le_mul_left_iff h0 hne, Order.one_le_iff_ne_zero]
   assumption
 
 lemma self_le_mul_left (a : ℕ∞) (hc : c ≠ 0) : a ≤ c * a := by
diff --git a/Mathlib/Data/ENat/Lattice.lean b/Mathlib/Data/ENat/Lattice.lean
@@ -69,16 +69,16 @@ lemma iInf_toNat : (⨅ i, (f i : ℕ∞)).toNat = ⨅ i, f i := by
   · norm_cast
 
 @[simp] lemma iInf_eq_zero {f : ι → ℕ∞} : ⨅ i, f i = 0 ↔ ∃ i, f i = 0 := by
-  simpa [lt_one_iff_eq_zero] using iInf_lt_iff (α := ℕ∞) (a := 1)
+  simpa [Order.lt_one_iff] using iInf_lt_iff (α := ℕ∞) (a := 1)
 
 variable {f : ι → ℕ∞} {s : Set ℕ∞}
 
 lemma sSup_eq_zero : sSup s = 0 ↔ ∀ a ∈ s, a = 0 :=
   sSup_eq_bot
 
 lemma sInf_eq_zero : sInf s = 0 ↔ 0 ∈ s := by
-  rw [← lt_one_iff_eq_zero]
-  simp only [sInf_lt_iff, lt_one_iff_eq_zero, exists_eq_right]
+  rw [← Order.lt_one_iff, sInf_lt_iff]
+  simp
 
 lemma sSup_eq_zero' : sSup s = 0 ↔ s = ∅ ∨ s = {0} :=
   sSup_eq_bot'
diff --git a/Mathlib/Data/ENat/Pow.lean b/Mathlib/Data/ENat/Pow.lean
@@ -84,63 +84,66 @@ lemma epow_right_mono (h : x ≠ 0) : Monotone (fun y : ℕ∞ ↦ x ^ y) := by
   · rw [top_le_iff.1 y_z]
   induction z
   · rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-    · exact (h (lt_one_iff_eq_zero.1 x_0)).rec
+    · exact (h (Order.lt_one_iff.1 x_0)).rec
     · simp only [one_epow, le_refl]
     · simp only [epow_top x_2, le_top]
-  · exact pow_right_mono₀ (one_le_iff_ne_zero.2 h) (Nat.cast_le.1 y_z)
+  · exact pow_right_mono₀ (Order.one_le_iff_ne_zero.2 h) (Nat.cast_le.1 y_z)
 
 lemma one_le_epow (h : x ≠ 0) : 1 ≤ x ^ y := by
   simpa using epow_right_mono h zero_le
 
+lemma epow_pos (h : x ≠ 0) : 0 < x ^ y := by
+  rw [← Order.one_le_iff_pos]; exact one_le_epow h
+
 lemma epow_left_mono : Monotone (fun x : ℕ∞ ↦ x ^ y) := by
   intro x z x_z
   simp only
   induction y
   · rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-    · rw [lt_one_iff_eq_zero.1 x_0, zero_epow_top]; exact bot_le
-    · rw [one_epow]; exact one_le_epow (one_le_iff_ne_zero.1 x_z)
+    · rw [Order.lt_one_iff.1 x_0, zero_epow_top]; exact bot_le
+    · rw [one_epow]; exact one_le_epow (Order.one_le_iff_ne_zero.1 x_z)
     · rw [epow_top (x_2.trans_le x_z)]; exact le_top
   · simp only [epow_natCast, (pow_left_mono _) x_z]
 
 lemma epow_eq_zero_iff : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0 := by
   refine ⟨fun h ↦ ⟨?_, fun y_0 ↦ ?_⟩, fun h ↦ h.1.symm ▸ zero_epow h.2⟩
-  · by_contra x_0
-    exact (one_le_iff_ne_zero.1 (one_le_epow (y := y) x_0) h).rec
+  · contrapose! h
+    exact (epow_pos h).ne'
   · rw [y_0, epow_zero] at h; contradiction
 
 lemma epow_eq_one_iff : x ^ y = 1 ↔ x = 1 ∨ y = 0 := by
   refine ⟨fun h ↦ or_iff_not_imp_right.2 fun y_0 ↦ ?_, fun h ↦ by rcases h with h | h <;> simp [h]⟩
   rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-  · rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0] at h; contradiction
+  · rw [Order.lt_one_iff.1 x_0, zero_epow y_0] at h; contradiction
   · rfl
-  · have := epow_right_mono (one_le_iff_ne_zero.1 x_2.le) (one_le_iff_ne_zero.2 y_0)
+  · have := epow_right_mono x_2.ne_zero (Order.one_le_iff_ne_zero.2 y_0)
     simp only [epow_one, h] at this
     exact (not_lt_of_ge this x_2).rec
 
 lemma epow_add : x ^ (y + z) = x ^ y * x ^ z := by
   rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-  · rw [lt_one_iff_eq_zero.1 x_0]
+  · rw [Order.lt_one_iff.1 x_0]
     rcases eq_zero_or_pos y with rfl | y_0
     · simp only [zero_add, epow_zero, one_mul]
     · rw [zero_epow y_0.ne.symm, zero_mul]
       exact zero_epow (add_pos_of_pos_of_nonneg y_0 bot_le).ne.symm
   · simp only [one_epow, mul_one]
   · induction y
     · rw [top_add, epow_top x_2, top_mul]
-      exact one_le_iff_ne_zero.1 (one_le_epow (one_le_iff_ne_zero.1 x_2.le))
+      exact (epow_pos x_2.ne_zero).ne'
     induction z
     · rw [add_top, epow_top x_2, mul_top]
-      exact one_le_iff_ne_zero.1 (one_le_epow (one_le_iff_ne_zero.1 x_2.le))
+      exact (epow_pos x_2.ne_zero).ne'
     simp only [← Nat.cast_add, epow_natCast, pow_add x]
 
 set_option backward.isDefEq.respectTransparency false in
 lemma mul_epow : (x * y) ^ z = x ^ z * y ^ z := by
   induction z
   · rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-    · simp only [lt_one_iff_eq_zero.1 x_0, zero_mul, zero_epow_top]
+    · simp only [Order.lt_one_iff.1 x_0, zero_mul, zero_epow_top]
     · simp only [one_mul, one_epow]
     · rcases lt_trichotomy y 1 with y_0 | rfl | y_2
-      · simp only [lt_one_iff_eq_zero.1 y_0, mul_zero, zero_epow_top]
+      · simp only [Order.lt_one_iff.1 y_0, mul_zero, zero_epow_top]
       · simp
       · rw [epow_top x_2, epow_top y_2, WithTop.top_mul_top]
         exact epow_top (one_lt_mul x_2.le y_2)
@@ -152,15 +155,14 @@ lemma epow_mul : x ^ (y * z) = (x ^ y) ^ z := by
   rcases eq_or_ne z 0 with z_0 | z_0
   · simp [z_0]
   rcases lt_trichotomy x 1 with x_0 | rfl | x_2
-  · rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]
+  · rw [Order.lt_one_iff.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]
   · simp only [one_epow]
   · induction y
     · rw [top_mul z_0, epow_top x_2, top_epow z_0]
     induction z
-    · rw [mul_top y_0, epow_top x_2]
-      apply (epow_top _).symm
-      apply (epow_right_mono (one_le_iff_ne_zero.1 x_2.le) (one_le_iff_ne_zero.2 y_0)).trans_lt'
-      simp only [x_2, epow_one]
+    · rw [mul_top y_0, epow_top x_2, epow_top]
+      apply (epow_right_mono x_2.ne_zero (Order.one_le_iff_ne_zero.2 y_0)).trans_lt'
+      simp [x_2]
     · simp only [← Nat.cast_mul, epow_natCast, pow_mul x]
 
 end ENat
diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
@@ -204,9 +204,9 @@ theorem encard_diff (h : s ⊆ t) (hs : s.Finite) :
   exact (ENat.addLECancellable_of_ne_top <| encard_ne_top_iff.mpr hs).eq_tsub_of_add_eq rfl
 
 @[simp] theorem one_le_encard_iff_nonempty : 1 ≤ s.encard ↔ s.Nonempty := by
-  rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, ENat.one_le_iff_ne_zero]
+  rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, Order.one_le_iff_ne_zero]
 
-@[simp] lemma encard_lt_one : s.encard < 1 ↔ s = ∅ := by simp [← not_le, not_nonempty_iff_eq_empty]
+lemma encard_lt_one : s.encard < 1 ↔ s = ∅ := by simp
 
 theorem encard_diff_add_encard_inter (s t : Set α) :
     (s \ t).encard + (s ∩ t).encard = s.encard := by
@@ -294,7 +294,7 @@ theorem encard_insert_le (s : Set α) (x : α) : (insert x s).encard ≤ s.encar
   rw [← union_singleton, ← encard_singleton x]; apply encard_union_le
 
 theorem one_le_encard_insert (s : Set α) : 1 ≤ (insert a s).encard :=
-  ENat.one_le_iff_ne_zero.mpr <| encard_ne_zero_of_mem (mem_insert a s)
+  Order.one_le_iff_ne_zero.mpr <| encard_ne_zero_of_mem (mem_insert a s)
 
 theorem encard_singleton_inter (s : Set α) (x : α) : ({x} ∩ s).encard ≤ 1 := by
   grw [← encard_singleton x, inter_subset_left]
@@ -356,7 +356,7 @@ theorem encard_eq_one : s.encard = 1 ↔ ∃ x, s = {x} := by
   exact ⟨x, ((finite_singleton x).eq_of_subset_of_encard_le (by simpa) (by simp [h])).symm⟩
 
 theorem encard_le_one_iff_eq : s.encard ≤ 1 ↔ s = ∅ ∨ ∃ x, s = {x} := by
-  rw [le_iff_lt_or_eq, lt_iff_not_ge, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
+  rw [le_iff_lt_or_eq, lt_iff_not_ge, Order.one_le_iff_ne_zero, not_not, encard_eq_zero,
     encard_eq_one]
 
 theorem encard_le_one_iff : s.encard ≤ 1 ↔ ∀ a b, a ∈ s → b ∈ s → a = b := by
diff --git a/Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean b/Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
@@ -250,7 +250,7 @@ lemma coverMincard_eq_zero_iff (T : X → X) (F : Set X) (U : SetRel X X) (n : 
 
 lemma one_le_coverMincard_iff (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ) :
     1 ≤ coverMincard T F U n ↔ F.Nonempty := by
-  rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty, not_iff_not]
+  rw [Order.one_le_iff_ne_zero, nonempty_iff_ne_empty, not_iff_not]
   exact coverMincard_eq_zero_iff T F U n
 
 lemma coverMincard_zero (T : X → X) (h : F.Nonempty) (U : SetRel X X) :
diff --git a/Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean b/Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
@@ -169,7 +169,7 @@ lemma netMaxcard_eq_zero_iff (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ
 
 lemma one_le_netMaxcard_iff (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ) :
     1 ≤ netMaxcard T F U n ↔ F.Nonempty := by
-  rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty]
+  rw [Order.one_le_iff_ne_zero, nonempty_iff_ne_empty]
   exact not_iff_not.2 (netMaxcard_eq_zero_iff T F U n)
 
 lemma netMaxcard_zero (T : X → X) (h : F.Nonempty) (U : SetRel X X) : netMaxcard T F U 0 = 1 := by
diff --git a/Mathlib/Order/Height.lean b/Mathlib/Order/Height.lean
diff --git a/Mathlib/RingTheory/Ideal/Height.lean b/Mathlib/RingTheory/Ideal/Height.lean
diff --git a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
diff --git a/Mathlib/RingTheory/MvPowerSeries/Order.lean b/Mathlib/RingTheory/MvPowerSeries/Order.lean
diff --git a/Mathlib/RingTheory/PowerSeries/Order.lean b/Mathlib/RingTheory/PowerSeries/Order.lean
diff --git a/Mathlib/SetTheory/Cardinal/ENat.lean b/Mathlib/SetTheory/Cardinal/ENat.lean
diff --git a/Mathlib/SetTheory/Cardinal/Finite.lean b/Mathlib/SetTheory/Cardinal/Finite.lean
