feat(Fin): conversion lemmas between Finset.Ixx (leanprover-community#33127)

This PR adds lemmas relating the various `Finset.Ixx` over `Fin n` when the endpoints differ by one.

Author: dupuisf

Mathlib/Order/Interval/Finset/Fin.lean

@@ -896,4 +896,79 @@ theorem card_Iio : #(Iio b) = b := by rw [← Nat.card_Iio b, ← map_valEmbeddi
 
 end card
 
+/-! ### Perturbations of endpoints by one -/
+
+/-
+Note: the `haveI`s in the statements below are needed for `0` and `1`
+to be defined in `Fin n`. One could instead add `[NeZero n]` at the
+top of this section, but then this instance would be required to
+rewrite using the lemmas.
+-/
+
+section pm_one
+
+lemma Iio_add_one_eq_Iic {n : ℕ} {b : Fin n} (hb : b + 1 < n) :
+    haveI := b.neZero
+    Iio (b + 1) = Iic b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']
+
+lemma Iic_sub_one_eq_Iio {n : ℕ} {b : Fin n} :
+    haveI := b.neZero
+    (hb : 0 < b) → Iic (b - 1) = Iio b := by
+  haveI := b.neZero
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]
+
+lemma Ici_add_one_eq_Ioi {n : ℕ} {a : Fin n} (ha : a + 1 < n) :
+    haveI := a.neZero
+    Ici (a + 1) = Ioi a := by
+  haveI := a.neZero
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']
+
+lemma Ioi_sub_one_eq_Ici {n : ℕ} {a : Fin n} :
+    haveI := a.neZero
+    (ha : 0 < a) → Ioi (a - 1) = Ici a := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]
+
+lemma Ioc_sub_one_eq_Icc {n : ℕ} {a b : Fin n} :
+    haveI := a.neZero
+    (ha : 0 < a) → Ioc (a - 1) b = Icc a b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]
+
+lemma Icc_add_one_eq_Ioc {n : ℕ} {a b : Fin n} (ha : a + 1 < n) :
+    haveI := a.neZero
+    Icc (a + 1) b = Ioc a b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']
+
+lemma Ioo_sub_one_eq_Ico {n : ℕ} {a b : Fin n} :
+    haveI := a.neZero
+    (ha : 0 < a) → Ioo (a - 1) b = Ico a b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]
+
+lemma Ico_add_one_eq_Ioo {n : ℕ} {a b : Fin n} (ha : a + 1 < n) :
+    haveI := a.neZero
+    Ico (a + 1) b = Ioo a b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']
+
+lemma Icc_sub_one_eq_Ico {n : ℕ} {a b : Fin n} :
+    haveI := a.neZero
+    (hb : 0 < b) → Icc a (b - 1) = Ico a b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]
+
+lemma Ico_add_one_eq_Icc {n : ℕ} {a b : Fin n} (hb : b + 1 < n) :
+    haveI := a.neZero
+    Ico a (b + 1) = Icc a b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']
+
+lemma Ioc_sub_one_eq_Ioo {n : ℕ} {a b : Fin n} :
+    haveI := a.neZero
+    (hb : 0 < b) → Ioc a (b - 1) = Ioo a b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]
+
+lemma Ioo_add_one_eq_Ioc {n : ℕ} {a b : Fin n} (hb : b + 1 < n) :
+    haveI := a.neZero
+    Ioo a (b + 1) = Ioc a b := by
+  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']
+
+end pm_one
+
 end Fin