feat(Order): Fin.succAboveOrderIso

Mathlib.lean

@@ -4243,6 +4243,7 @@ import Mathlib.Order.Filter.Ultrafilter.Defs
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 import Mathlib.Order.Fin.Basic
 import Mathlib.Order.Fin.Finset
+import Mathlib.Order.Fin.SuccAboveOrderIso
 import Mathlib.Order.Fin.Tuple
 import Mathlib.Order.FixedPoints
 import Mathlib.Order.GaloisConnection.Basic

Mathlib/Data/Fin/Basic.lean

@@ -1282,6 +1282,17 @@ lemma succAbove_predAbove {p : Fin n} {i : Fin (n + 1)} (h : i ≠ castSucc p) :
   · rw [predAbove_of_le_castSucc _ _ (Fin.le_of_lt h), succAbove_castPred_of_lt _ _ h]
   · rw [predAbove_of_castSucc_lt _ _ h, succAbove_pred_of_lt _ _ h]
 
+/-- Sending `Fin (n+1)` to `Fin n` by subtracting one from anything above `p`
+then back to `Fin (n+1)` with a gap around `p.succ` is the identity away from `p.succ`. -/
+@[simp]
+lemma succ_succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.succ) :
+    p.succ.succAbove (p.predAbove i) = i := by
+  obtain h | h := Fin.lt_or_lt_of_ne h
+  · rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h),
+      succAbove_castPred_of_lt _ _ h]
+  · rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
+      succAbove_pred_of_lt _ _ h]
+
 /-- Sending `Fin n` into `Fin (n + 1)` with a gap at `p`
 then back to `Fin n` by subtracting one from anything above `p` is the identity. -/
 @[simp]

Mathlib/Order/Fin/SuccAboveOrderIso.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import Mathlib.Order.Fin.Basic
+import Mathlib.Data.Fintype.Basic
+import Mathlib.Tactic.FinCases
+
+/-!
+# The order isomorphism `Fin (n + 1) ≃o {i}ᶜ`
+
+Given `i : Fin (n + 2)`, we show that `Fin.succAboveOrderEmb` induces
+an order isomorphism `Fin (n + 1) ≃o ({i}ᶜ : Finset (Fin (n + 2)))`.
+
+-/
+
+open Finset
+
+/-- Given `i : Fin (n + 2)`, this is the order isomorphism
+between `Fin (n + 1)` and the finite set `{i}ᶜ`. -/
+noncomputable def Fin.succAboveOrderIso {n : ℕ} (i : Fin (n + 2)) :
+    Fin (n + 1) ≃o ({i}ᶜ : Finset (Fin (n + 2))) where
+  toEquiv :=
+    Equiv.ofBijective (f := fun a ↦ ⟨Fin.succAboveOrderEmb i a,
+        by simpa using Fin.succAbove_ne i a⟩) (by
+      constructor
+      · intro a b h
+        exact (Fin.succAboveOrderEmb i).injective (by simpa using h)
+      · rintro ⟨j, hj⟩
+        simp only [mem_compl, mem_singleton] at hj
+        obtain rfl | ⟨i, rfl⟩ := Fin.eq_zero_or_eq_succ i
+        · exact ⟨j.pred hj, by simp⟩
+        · exact ⟨i.predAbove j, by aesop⟩)
+  map_rel_iff' {a b} := by
+    simp only [Equiv.ofBijective_apply, Subtype.mk_le_mk, OrderEmbedding.le_iff_le]