From 696c3090c8caa15d9d7cc2603e90f774c861cafa Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 19 Mar 2026 00:23:18 +0800
Subject: [PATCH 01/10] add lemma about WithBot ENat

---
 Mathlib/Algebra/Order/Monoid/WithTop.lean |  6 ++++++
 Mathlib/Data/ENat/Basic.lean              | 14 ++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean
index c15812a0ffbe9f..2fb7a2f665b5be 100644
--- a/Mathlib/Algebra/Order/Monoid/WithTop.lean
+++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean
@@ -64,4 +64,10 @@ protected theorem le_add_self [AddCommMagma α] [LE α] [CanonicallyOrderedAdd 
   · rw [← WithBot.coe_add, WithBot.coe_le_coe]
     exact le_add_self
 
+lemma lt_zero_iff_eq_bot {α : Type*} [AddMonoid α] [Preorder α] [CanonicallyOrderedAdd α]
+    (a : WithBot α) : a < 0 ↔ a = ⊥ := by
+  induction a with
+  | bot => simp
+  | coe => simp
+
 end WithBot
diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index c436ec43f4aab8..79574ac7b2350f 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -619,6 +619,8 @@ end ENat
 
 namespace ENat.WithBot
 
+lemma coe_eq_natCast (n : ℕ) : (n : ℕ∞) = (n : WithBot ℕ∞) := rfl
+
 lemma lt_add_one_iff {n : WithBot ℕ∞} {m : ℕ} : n < m + 1 ↔ n ≤ m := by
   rw [← WithBot.coe_one, ← ENat.coe_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]
   cases n
@@ -633,6 +635,18 @@ lemma add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n < m := b
   · rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
       ← WithBot.coe_lt_coe, WithBot.coe_natCast]
 
+lemma add_one_le_natCast_iff (n : WithBot ℕ∞) (m : ℕ) : n + 1 ≤ m ↔ n < m := by
+  induction n with
+  | bot => simp
+  | coe n =>
+    by_cases eq : n = ⊤
+    · simpa [eq] using WithBot.coe_lt_coe.mpr (ENat.coe_lt_top m)
+    · rw [← ENat.WithBot.coe_eq_natCast, ← WithBot.coe_one, ← WithBot.coe_add, WithBot.coe_le_coe,
+        WithBot.coe_lt_coe, ENat.add_one_le_iff eq]
+
+lemma add_one_le_zero_iff (n : WithBot ℕ∞) : n + 1 ≤ 0 ↔ n = ⊥ :=
+  (add_one_le_natCast_iff n 0).trans (WithBot.lt_zero_iff_eq_bot n)
+
 @[simp]
 lemma add_natCast_cancel {a b : WithBot ℕ∞} {c : ℕ} : a + c = b + c ↔ a = b :=
   (IsAddRightRegular.all c).withTop.withBot.eq_iff

From f57b3afb666c5f2e487944b049a9d34e58bed2df Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 19 Mar 2026 14:33:42 +0800
Subject: [PATCH 02/10] golf

---
 Mathlib/Algebra/Order/Monoid/WithTop.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean
index 2fb7a2f665b5be..8d54a9ce9776f2 100644
--- a/Mathlib/Algebra/Order/Monoid/WithTop.lean
+++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean
@@ -66,8 +66,6 @@ protected theorem le_add_self [AddCommMagma α] [LE α] [CanonicallyOrderedAdd 
 
 lemma lt_zero_iff_eq_bot {α : Type*} [AddMonoid α] [Preorder α] [CanonicallyOrderedAdd α]
     (a : WithBot α) : a < 0 ↔ a = ⊥ := by
-  induction a with
-  | bot => simp
-  | coe => simp
+  induction a <;> simp
 
 end WithBot

From 2539428e6b6d76cdec7d35d8f2478657adb35542 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 19 Mar 2026 14:47:12 +0800
Subject: [PATCH 03/10] add ENat preliminary

and golf
---
 Mathlib/Data/ENat/Basic.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 79574ac7b2350f..706e6e85aff5f0 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -292,6 +292,11 @@ theorem succ_def (m : ℕ∞) : Order.succ m = m + 1 :=
 theorem add_one_le_iff (hm : m ≠ ⊤) : m + 1 ≤ n ↔ m < n :=
   Order.add_one_le_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)
 
+theorem add_one_le_iff' (hn : n ≠ ⊤) : m + 1 ≤ n ↔ m < n := by
+  by_cases hm : m = ⊤
+  · simpa [hm]
+  · 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
 
@@ -639,10 +644,7 @@ lemma add_one_le_natCast_iff (n : WithBot ℕ∞) (m : ℕ) : n + 1 ≤ m ↔ n
   induction n with
   | bot => simp
   | coe n =>
-    by_cases eq : n = ⊤
-    · simpa [eq] using WithBot.coe_lt_coe.mpr (ENat.coe_lt_top m)
-    · rw [← ENat.WithBot.coe_eq_natCast, ← WithBot.coe_one, ← WithBot.coe_add, WithBot.coe_le_coe,
-        WithBot.coe_lt_coe, ENat.add_one_le_iff eq]
+    simp [← coe_eq_natCast, ← WithBot.coe_one, ← WithBot.coe_add, add_one_le_iff']
 
 lemma add_one_le_zero_iff (n : WithBot ℕ∞) : n + 1 ≤ 0 ↔ n = ⊥ :=
   (add_one_le_natCast_iff n 0).trans (WithBot.lt_zero_iff_eq_bot n)

From e358eede88d3d2bcefc700eefbc9cc0c6057f790 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Fri, 27 Mar 2026 09:12:01 +0800
Subject: [PATCH 04/10] golf

---
 Mathlib/Data/ENat/Basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 83bd747cfe443e..6bb00b0b8f201f 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -649,7 +649,8 @@ lemma add_one_le_natCast_iff (n : WithBot ℕ∞) (m : ℕ) : n + 1 ≤ m ↔ n
   induction n with
   | bot => simp
   | coe n =>
-    simp [← coe_eq_natCast, ← WithBot.coe_one, ← WithBot.coe_add, add_one_le_iff']
+    norm_cast
+    simp [add_one_le_iff']
 
 lemma add_one_le_zero_iff (n : WithBot ℕ∞) : n + 1 ≤ 0 ↔ n = ⊥ :=
   (add_one_le_natCast_iff n 0).trans (WithBot.lt_zero_iff_eq_bot n)

From 89c3cbb523a5983f0edbb56ed98f21749fef36ec Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Fri, 27 Mar 2026 09:12:24 +0800
Subject: [PATCH 05/10] add simp attr

---
 Mathlib/Data/ENat/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 6bb00b0b8f201f..12d3334a18e9cb 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -629,6 +629,7 @@ end ENat
 
 namespace ENat.WithBot
 
+@[simp]
 lemma coe_eq_natCast (n : ℕ) : (n : ℕ∞) = (n : WithBot ℕ∞) := rfl
 
 lemma lt_add_one_iff {n : WithBot ℕ∞} {m : ℕ} : n < m + 1 ↔ n ≤ m := by

From d8807177a6bebbcd809fdbb2d87762758102f55c Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 2 Apr 2026 15:18:24 +0800
Subject: [PATCH 06/10] fix variable

---
 Mathlib/Data/ENat/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 11b3fd80e89f4a..8f2b18a2aa8f42 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -629,7 +629,7 @@ lemma add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n < m := b
   · rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
       ← WithBot.coe_lt_coe, WithBot.coe_natCast]
 
-lemma add_one_le_natCast_iff (n : WithBot ℕ∞) (m : ℕ) : n + 1 ≤ m ↔ n < m := by
+lemma add_one_le_natCast_iff {n : WithBot ℕ∞} {m : ℕ} : n + 1 ≤ m ↔ n < m := by
   induction n with
   | bot => simp
   | coe n =>

From f4260bf8577104ca685017ae491a84a2595a64a7 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 2 Apr 2026 15:54:11 +0800
Subject: [PATCH 07/10] golf

---
 Mathlib/Data/ENat/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 8f2b18a2aa8f42..d3835f2ec3b57f 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -281,7 +281,7 @@ theorem add_one_le_iff (hm : m ≠ ⊤) : m + 1 ≤ n ↔ m < n :=
 
 theorem add_one_le_iff' (hn : n ≠ ⊤) : m + 1 ≤ n ↔ m < n := by
   by_cases hm : m = ⊤
-  · simpa [hm]
+  · simp_all
   · exact add_one_le_iff hm
 
 theorem one_le_iff_ne_zero : 1 ≤ n ↔ n ≠ 0 :=

From ea39aa6be1f0fe38fbc9022bd6f94023be49c1f8 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 2 Apr 2026 16:05:46 +0800
Subject: [PATCH 08/10] fix

---
 Mathlib/Data/ENat/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index d3835f2ec3b57f..29796bca313ee2 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -637,7 +637,7 @@ lemma add_one_le_natCast_iff {n : WithBot ℕ∞} {m : ℕ} : n + 1 ≤ m ↔ n
     simp [add_one_le_iff']
 
 lemma add_one_le_zero_iff (n : WithBot ℕ∞) : n + 1 ≤ 0 ↔ n = ⊥ :=
-  (add_one_le_natCast_iff n 0).trans (WithBot.lt_zero_iff_eq_bot n)
+  add_one_le_natCast_iff.trans (WithBot.lt_zero_iff_eq_bot n)
 
 @[simp]
 lemma add_natCast_cancel {a b : WithBot ℕ∞} {c : ℕ} : a + c = b + c ↔ a = b :=

From 931651fccf0555d83de08223fe31b5d2f4f046c7 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 2 Apr 2026 18:13:06 +0800
Subject: [PATCH 09/10] add simp attr

---
 Mathlib/Data/ENat/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 29796bca313ee2..452199a2c5ad77 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -636,6 +636,7 @@ lemma add_one_le_natCast_iff {n : WithBot ℕ∞} {m : ℕ} : n + 1 ≤ m ↔ n
     norm_cast
     simp [add_one_le_iff']
 
+@[simp]
 lemma add_one_le_zero_iff (n : WithBot ℕ∞) : n + 1 ≤ 0 ↔ n = ⊥ :=
   add_one_le_natCast_iff.trans (WithBot.lt_zero_iff_eq_bot n)
 

From 7baacbdc6f1a2ec5a162b08f85b4863337a55322 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Thu, 2 Apr 2026 18:13:31 +0800
Subject: [PATCH 10/10] golf

---
 Mathlib/Data/ENat/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 452199a2c5ad77..423e99d10d634e 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -280,8 +280,8 @@ theorem add_one_le_iff (hm : m ≠ ⊤) : m + 1 ≤ n ↔ m < n :=
   Order.add_one_le_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)
 
 theorem add_one_le_iff' (hn : n ≠ ⊤) : m + 1 ≤ n ↔ m < n := by
-  by_cases hm : m = ⊤
-  · simp_all
+  rcases eq_or_ne m ⊤ with rfl | hm
+  · simpa
   · exact add_one_le_iff hm
 
 theorem one_le_iff_ne_zero : 1 ≤ n ↔ n ≠ 0 :=