From 8cacd8e630489d9ac95505aec561c3accd6b4cee Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Fri, 27 Sep 2024 17:57:33 +0000
Subject: [PATCH] =?UTF-8?q?feat:=20a=20few=20lemmas=20on=20`WithTop=20?=
 =?UTF-8?q?=E2=84=95=E2=88=9E`=20(#17164)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

To be used when `WithTop ℕ∞` becomes the set of smoothness exponents, in #17152
---
 Mathlib/Data/ENat/Basic.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 1ff8e427f3cb9c..3486a11a1cef21 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -259,4 +259,26 @@ theorem nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀
   · exact htop A
   · exact A _
 
+lemma add_one_nat_le_withTop_of_lt {m : ℕ} {n : WithTop ℕ∞} (h : m < n) : (m + 1 : ℕ) ≤ n := by
+  match n with
+  | ⊤ => exact le_top
+  | (⊤ : ℕ∞) => exact WithTop.coe_le_coe.2 (OrderTop.le_top _)
+  | (n : ℕ) => simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using h
+
+@[simp] lemma coe_top_add_one : ((⊤ : ℕ∞) : WithTop ℕ∞) + 1 = (⊤ : ℕ∞) := rfl
+
+@[simp] lemma add_one_eq_coe_top_iff (n : WithTop ℕ∞) :
+    n + 1 = (⊤ : ℕ∞) ↔ n = (⊤ : ℕ∞) := by
+  match n with
+  | ⊤ => exact Iff.rfl
+  | (⊤ : ℕ∞) => exact Iff.rfl
+  | (n : ℕ) => norm_cast; simp only [coe_ne_top, iff_false, ne_eq]
+
+@[simp] lemma nat_ne_coe_top (n : ℕ) : (n : WithTop ℕ∞) ≠ (⊤ : ℕ∞) := ne_of_beq_false rfl
+
+lemma one_le_iff_ne_zero_withTop {n : WithTop ℕ∞} :
+    1 ≤ n ↔ n ≠ 0 :=
+  ⟨fun h ↦ (zero_lt_one.trans_le h).ne',
+    fun h ↦ add_one_nat_le_withTop_of_lt (pos_iff_ne_zero.mpr h)⟩
+
 end ENat