feat: the successor as a function WithBot α → α (#20055)

This will be useful to do induction on a family of polynomials by the sum of the successor of their degree.

From GrowthInGroups (LeanCamCombi)

Co-authored-by: Andrew Yang

Author: YaelDillies

Mathlib.lean

@@ -775,6 +775,7 @@ import Mathlib.Algebra.Order.Sub.Unbundled.Hom
 import Mathlib.Algebra.Order.Sub.WithTop
 import Mathlib.Algebra.Order.SuccPred
 import Mathlib.Algebra.Order.SuccPred.TypeTags
+import Mathlib.Algebra.Order.SuccPred.WithBot
 import Mathlib.Algebra.Order.Sum
 import Mathlib.Algebra.Order.ToIntervalMod
 import Mathlib.Algebra.Order.UpperLower
@@ -4175,6 +4176,7 @@ import Mathlib.Order.SuccPred.Limit
 import Mathlib.Order.SuccPred.LinearLocallyFinite
 import Mathlib.Order.SuccPred.Relation
 import Mathlib.Order.SuccPred.Tree
+import Mathlib.Order.SuccPred.WithBot
 import Mathlib.Order.SupClosed
 import Mathlib.Order.SupIndep
 import Mathlib.Order.SymmDiff

Mathlib/Algebra/Order/SuccPred/WithBot.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2024 Yaël Dillies, Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Andrew Yang
+-/
+import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
+import Mathlib.Algebra.Order.SuccPred
+import Mathlib.Order.SuccPred.WithBot
+
+/-!
+# Algebraic properties of the successor function on `WithBot`
+-/
+
+namespace WithBot
+variable {α : Type*} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α]
+
+lemma succ_natCast (n : ℕ) : succ (n : WithBot α) = n + 1 := by
+  rw [← WithBot.coe_natCast, succ_coe, Order.succ_eq_add_one]
+
+@[simp] lemma succ_zero : succ (0 : WithBot α) = 1 := by simpa using succ_natCast 0
+
+@[simp]
+lemma succ_one : succ (1 : WithBot α) = 2 := by simpa [one_add_one_eq_two] using succ_natCast 1
+
+@[simp]
+lemma succ_ofNat (n : ℕ) [n.AtLeastTwo] :
+    succ (no_index (OfNat.ofNat n) : WithBot α) = OfNat.ofNat n + 1 := succ_natCast n
+
+end WithBot

Mathlib/Algebra/Polynomial/Splits.lean

@@ -77,7 +77,7 @@ theorem splits_of_degree_le_one {f : K[X]} (hf : degree f ≤ 1) : Splits i f :=
   if hif : degree (f.map i) ≤ 0 then splits_of_map_eq_C i (degree_le_zero_iff.mp hif)
   else by
     push_neg at hif
-    rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.succ_coe, Nat.succ_eq_succ] at hif
+    rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.orderSucc_coe, Nat.succ_eq_succ] at hif
     exact splits_of_map_degree_eq_one i ((degree_map_le.trans hf).antisymm hif)
 
 theorem splits_of_degree_eq_one {f : K[X]} (hf : degree f = 1) : Splits i f :=

Mathlib/Order/SuccPred/Basic.lean

@@ -1063,13 +1063,11 @@ instance : PredOrder (WithTop α) where
     · exact coe_le_coe.2 le_top
     exact coe_le_coe.2 (le_pred_of_lt <| coe_lt_coe.1 h)
 
-@[simp]
-theorem pred_top : pred (⊤ : WithTop α) = ↑(⊤ : α) :=
-  rfl
+/-- Not to be confused with `WithTop.pred_bot`, which is about `WithTop.pred`. -/
+@[simp] lemma orderPred_top : pred (⊤ : WithTop α) = ↑(⊤ : α) := rfl
 
-@[simp]
-theorem pred_coe (a : α) : pred (↑a : WithTop α) = ↑(pred a) :=
-  rfl
+/-- Not to be confused with `WithTop.pred_coe`, which is about `WithTop.pred`. -/
+@[simp] lemma orderPred_coe (a : α) : pred (↑a : WithTop α) = ↑(pred a) := rfl
 
 @[simp]
 theorem pred_untop :
@@ -1125,13 +1123,11 @@ instance : SuccOrder (WithBot α) where
     · exact coe_le_coe.2 bot_le
     · exact coe_le_coe.2 (succ_le_of_lt <| coe_lt_coe.1 h)
 
-@[simp]
-theorem succ_bot : succ (⊥ : WithBot α) = ↑(⊥ : α) :=
-  rfl
+/-- Not to be confused with `WithBot.succ_bot`, which is about `WithBot.succ`. -/
+@[simp] lemma orderSucc_bot : succ (⊥ : WithBot α) = ↑(⊥ : α) := rfl
 
-@[simp]
-theorem succ_coe (a : α) : succ (↑a : WithBot α) = ↑(succ a) :=
-  rfl
+/-- Not to be confused with `WithBot.succ_coe`, which is about `WithBot.succ`. -/
+@[simp] lemma orderSucc_coe (a : α) : succ (↑a : WithBot α) = ↑(succ a) := rfl
 
 @[simp]
 theorem succ_unbot :

Mathlib/Order/SuccPred/WithBot.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2024 Yaël Dillies, Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Andrew Yang
+-/
+import Mathlib.Order.SuccPred.Basic
+
+/-!
+# Successor function on `WithBot`
+
+This file defines the successor of `a : WithBot α` as an element of `α`, and dually for `WithTop`.
+-/
+
+namespace WithBot
+variable {α : Type*} [Preorder α] [OrderBot α] [SuccOrder α] {x y : WithBot α}
+
+/-- The successor of `a : WithBot α` as an element of `α`. -/
+def succ (a : WithBot α) : α := a.recBotCoe ⊥ Order.succ
+
+/-- Not to be confused with `WithBot.orderSucc_bot`, which is about `Order.succ`. -/
+@[simp] lemma succ_bot : succ (⊥ : WithBot α) = ⊥ := rfl
+
+/-- Not to be confused with `WithBot.orderSucc_coe`, which is about `Order.succ`. -/
+@[simp] lemma succ_coe (a : α) : succ (a : WithBot α) = Order.succ a := rfl
+
+lemma succ_eq_succ : ∀ a : WithBot α, succ a = Order.succ a
+  | ⊥ => rfl
+  | (a : α) => rfl
+
+lemma succ_mono : Monotone (succ : WithBot α → α)
+  | ⊥, _, _ => by simp
+  | (a : α), ⊥, hab => by simp at hab
+  | (a : α), (b : α), hab => Order.succ_le_succ (by simpa using hab)
+
+lemma succ_strictMono [NoMaxOrder α] : StrictMono (succ : WithBot α → α)
+  | ⊥, (b : α), hab => by simp
+  | (a : α), (b : α), hab => Order.succ_lt_succ (by simpa using hab)
+
+@[gcongr] lemma succ_le_succ (hxy : x ≤ y) : x.succ ≤ y.succ := succ_mono hxy
+@[gcongr] lemma succ_lt_succ [NoMaxOrder α] (hxy : x < y) : x.succ < y.succ := succ_strictMono hxy
+
+end WithBot
+
+namespace WithTop
+variable {α : Type*} [Preorder α] [OrderTop α] [PredOrder α] {x y : WithTop α}
+
+/-- The predessor of `a : WithTop α` as an element of `α`. -/
+def pred (a : WithTop α) : α := a.recTopCoe ⊤ Order.pred
+
+/-- Not to be confused with `WithTop.orderPred_top`, which is about `Order.pred`. -/
+@[simp] lemma pred_top : pred (⊤ : WithTop α) = ⊤ := rfl
+
+/-- Not to be confused with `WithTop.orderPred_coe`, which is about `Order.pred`. -/
+@[simp] lemma pred_coe (a : α) : pred (a : WithTop α) = Order.pred a := rfl
+
+lemma pred_eq_pred : ∀ a : WithTop α, pred a = Order.pred a
+  | ⊤ => rfl
+  | (a : α) => rfl
+
+lemma pred_mono : Monotone (pred : WithTop α → α)
+  | _, ⊤, _ => by simp
+  | ⊤, (a : α), hab => by simp at hab
+  | (a : α), (b : α), hab => Order.pred_le_pred (by simpa using hab)
+
+lemma pred_strictMono [NoMinOrder α] : StrictMono (pred : WithTop α → α)
+  | (b : α), ⊤, hab => by simp
+  | (a : α), (b : α), hab => Order.pred_lt_pred (by simpa using hab)
+
+@[gcongr] lemma pred_le_pred (hxy : x ≤ y) : x.pred ≤ y.pred := pred_mono hxy
+@[gcongr] lemma pred_lt_pred [NoMinOrder α] (hxy : x < y) : x.pred < y.pred := pred_strictMono hxy
+
+end WithTop