feat: simproc for computing Finset.Ixx of natural numbers

Mathlib.lean

@@ -4415,6 +4415,7 @@ import Mathlib.Order.Interval.Finset.Box
 import Mathlib.Order.Interval.Finset.Defs
 import Mathlib.Order.Interval.Finset.Fin
 import Mathlib.Order.Interval.Finset.Nat
+import Mathlib.Order.Interval.Finset.SuccPred
 import Mathlib.Order.Interval.Multiset
 import Mathlib.Order.Interval.Set.Basic
 import Mathlib.Order.Interval.Set.Defs
@@ -5348,6 +5349,7 @@ import Mathlib.Tactic.Set
 import Mathlib.Tactic.SetLike
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.SimpRw
+import Mathlib.Tactic.Simproc.FinsetInterval
 import Mathlib.Tactic.Simps.Basic
 import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SplitIfs

Mathlib/Algebra/Order/Interval/Finset.lean

@@ -5,19 +5,103 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Group.Embedding
 import Mathlib.Algebra.Order.Interval.Set.Monoid
-import Mathlib.Order.Interval.Finset.Defs
+import Mathlib.Algebra.Order.SuccPred
+import Mathlib.Order.Interval.Finset.SuccPred
 
 /-!
 # Algebraic properties of finset intervals
 
 This file provides results about the interaction of algebra with `Finset.Ixx`.
 -/
 
-open Function OrderDual
+open Function Order OrderDual
 
 variable {ι α : Type*}
 
 namespace Finset
+section LinearOrder
+variable [LinearOrder α] [LocallyFiniteOrder α] [One α]
+
+section SuccAddOrder
+variable [Add α] [SuccAddOrder α] {a b : α}
+
+lemma Ico_add_one_left_eq_Ioo (a b : α) : Ico (a + 1) b = Ioo a b := by
+  simpa [succ_eq_add_one] using Ico_succ_left_eq_Ioo a b
+
+lemma Icc_add_one_left_eq_Ioc_of_not_isMax (ha : ¬ IsMax a) (b : α) : Icc (a + 1) b = Ioc a b := by
+  simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc_of_not_isMax ha b
+
+lemma Ico_add_one_right_eq_Icc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ico a (b + 1) = Icc a b := by
+  simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc_of_not_isMax hb a
+
+lemma Ioo_add_one_right_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ioo a (b + 1) = Ioc a b := by
+  simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc_of_not_isMax hb a
+
+lemma Ico_add_one_add_one_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) :
+    Ico (a + 1) (b + 1) = Ioc a b := by
+  simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc_of_not_isMax hb a
+
+variable [NoMaxOrder α]
+
+lemma Icc_add_one_left_eq_Ioc (a b : α) : Icc (a + 1) b = Ioc a b := by
+  simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc a b
+
+lemma Ico_add_one_right_eq_Icc (a b : α) : Ico a (b + 1) = Icc a b := by
+  simpa [succ_eq_add_one] using  Ico_succ_right_eq_Icc a b
+
+lemma Ioo_add_one_right_eq_Ioc (a b : α) : Ioo a (b + 1) = Ioc a b := by
+  simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc a b
+
+lemma Ico_add_one_add_one_eq_Ioc (a b : α) : Ico (a + 1) (b + 1) = Ioc a b := by
+  simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc a b
+
+end SuccAddOrder
+
+section PredSubOrder
+variable [Sub α] [PredSubOrder α] {a b : α}
+
+lemma Ioc_sub_one_right_eq_Ioo (a b : α) : Ioc a (b - 1) = Ioo a b := by
+  simpa [pred_eq_sub_one] using Ioc_pred_right_eq_Ioo a b
+
+lemma Icc_sub_one_right_eq_Ico_of_not_isMin (hb : ¬ IsMin b) (a : α) : Icc a (b - 1) = Ico a b := by
+  simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico_of_not_isMin hb a
+
+lemma Ioc_sub_one_left_eq_Icc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioc (a - 1) b = Icc a b := by
+  simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc_of_not_isMin ha b
+
+lemma Ioo_sub_one_left_eq_Ioc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioo (a - 1) b = Ico a b := by
+  simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc_of_not_isMin ha b
+
+lemma Ioc_sub_one_sub_one_eq_Ico_of_not_isMin (ha : ¬ IsMin a) (b : α) :
+    Ioc (a - 1) (b - 1) = Ico a b := by
+  simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico_of_not_isMin ha b
+
+variable [NoMinOrder α]
+
+lemma Icc_sub_one_right_eq_Ico (a b : α) : Icc a (b - 1) = Ico a b := by
+  simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico a b
+
+lemma Ioc_sub_one_left_eq_Icc (a b : α) : Ioc (a - 1) b = Icc a b := by
+  simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc a b
+
+lemma Ioo_sub_one_left_eq_Ioc (a b : α) : Ioo (a - 1) b = Ico a b := by
+  simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc a b
+
+lemma Ioc_sub_one_sub_one_eq_Ico (a b : α) : Ioc (a - 1) (b - 1) = Ico a b := by
+  simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico a b
+
+end PredSubOrder
+
+section SuccAddPredSubOrder
+variable [Add α] [Sub α] [SuccAddOrder α] [PredSubOrder α] [Nontrivial α]
+
+lemma Icc_add_one_sub_one_eq_Ioo (a b : α) : Icc (a + 1) (b - 1) = Ioo a b := by
+  simpa [succ_eq_add_one, pred_eq_sub_one] using Icc_succ_pred_eq_Ioo a b
+
+end SuccAddPredSubOrder
+
+end LinearOrder
+
 variable [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α]
 
 @[simp] lemma map_add_left_Icc (a b c : α) :

Mathlib/Order/Interval/Finset/Nat.lean

@@ -101,42 +101,51 @@ theorem card_fintypeIic : Fintype.card (Set.Iic b) = b + 1 := by
 
 theorem card_fintypeIio : Fintype.card (Set.Iio b) = b := by rw [Fintype.card_ofFinset, card_Iio]
 
--- TODO@Yaël: Generalize all the following lemmas to `SuccOrder`
+@[deprecated "Use `Finset.Icc_succ_left_eq_Ioc`" (since := "2025-02-25")]
 theorem Icc_succ_left : Icc a.succ b = Ioc a b := by
   ext x
   rw [mem_Icc, mem_Ioc, succ_le_iff]
 
+@[deprecated "Use `Finset.Ico_succ_right_eq_Icc`" (since := "2025-02-25")]
 theorem Ico_succ_right : Ico a b.succ = Icc a b := by
   ext x
   rw [mem_Ico, mem_Icc, Nat.lt_succ_iff]
 
+@[deprecated "Use `Finset.Ico_succ_left_eq_Ioo`" (since := "2025-02-25")]
 theorem Ico_succ_left : Ico a.succ b = Ioo a b := by
   ext x
   rw [mem_Ico, mem_Ioo, succ_le_iff]
 
+@[deprecated "Use `Finset.Icc_pred_right_eq_Ico`" (since := "2025-02-25")]
 theorem Icc_pred_right {b : ℕ} (h : 0 < b) : Icc a (b - 1) = Ico a b := by
   ext x
   rw [mem_Icc, mem_Ico, lt_iff_le_pred h]
 
+@[deprecated "Use `Finset.Ico_succ_succ_eq_Ioc`" (since := "2025-02-25")]
 theorem Ico_succ_succ : Ico a.succ b.succ = Ioc a b := by
   ext x
   rw [mem_Ico, mem_Ioc, succ_le_iff, Nat.lt_succ_iff]
 
+set_option linter.deprecated false in
 @[simp]
 theorem Ico_succ_singleton : Ico a (a + 1) = {a} := by rw [Ico_succ_right, Icc_self]
 
+set_option linter.deprecated false in
 @[simp]
 theorem Ico_pred_singleton {a : ℕ} (h : 0 < a) : Ico (a - 1) a = {a - 1} := by
   rw [← Icc_pred_right _ h, Icc_self]
 
+set_option linter.deprecated false in
 @[simp]
 theorem Ioc_succ_singleton : Ioc b (b + 1) = {b + 1} := by rw [← Nat.Icc_succ_left, Icc_self]
 
 variable {a b c}
 
+set_option linter.deprecated false in
 theorem Ico_succ_right_eq_insert_Ico (h : a ≤ b) : Ico a (b + 1) = insert b (Ico a b) := by
   rw [Ico_succ_right, ← Ico_insert_right h]
 
+set_option linter.deprecated false in
 theorem Ico_insert_succ_left (h : a < b) : insert a (Ico a.succ b) = Ico a b := by
   rw [Ico_succ_left, ← Ioo_insert_left h]
 
@@ -166,6 +175,7 @@ theorem Ico_image_const_sub_eq_Ico (hac : a ≤ c) :
   rintro ⟨x, hx, rfl⟩
   omega
 
+set_option linter.deprecated false in
 theorem Ico_succ_left_eq_erase_Ico : Ico a.succ b = erase (Ico a b) a := by
   ext x
   rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← and_assoc, ne_comm,

Mathlib/Order/Interval/Finset/SuccPred.lean

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2025 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Algebra.Group.Embedding
+import Mathlib.Algebra.Order.Interval.Set.Monoid
+import Mathlib.Algebra.Order.SuccPred
+import Mathlib.Order.Interval.Finset.Basic
+
+open Order
+
+namespace Finset
+variable {α : Type*} [LinearOrder α] [LocallyFiniteOrder α]
+
+section SuccOrder
+variable [SuccOrder α] {a b : α}
+
+lemma Ico_succ_left_eq_Ioo (a b : α) : Ico (succ a) b = Ioo a b := by
+  by_cases ha : IsMax a
+  · rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]
+  · ext x
+    rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]
+
+lemma Icc_succ_left_eq_Ioc_of_not_isMax (ha : ¬ IsMax a) (b : α) : Icc (succ a) b = Ioc a b := by
+  ext x; rw [mem_Icc, mem_Ioc, succ_le_iff_of_not_isMax ha]
+
+lemma Ico_succ_right_eq_Icc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ico a (succ b) = Icc a b := by
+  ext x; rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]
+
+lemma Ioo_succ_right_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ioo a (succ b) = Ioc a b := by
+  ext x; rw [mem_Ioo, mem_Ioc, lt_succ_iff_of_not_isMax hb]
+
+lemma Ico_succ_succ_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) :
+    Ico (succ a) (succ b) = Ioc a b := by
+  rw [Ico_succ_left_eq_Ioo, Ioo_succ_right_eq_Ioc_of_not_isMax hb]
+
+variable [NoMaxOrder α]
+
+lemma Icc_succ_left_eq_Ioc (a b : α) : Icc (succ a) b = Ioc a b :=
+  Icc_succ_left_eq_Ioc_of_not_isMax (not_isMax _) _
+
+lemma Ico_succ_right_eq_Icc (a b : α) : Ico a (succ b) = Icc a b :=
+  Ico_succ_right_eq_Icc_of_not_isMax (not_isMax _) _
+
+lemma Ioo_succ_right_eq_Ioc (a b : α) : Ioo a (succ b) = Ioc a b :=
+  Ioo_succ_right_eq_Ioc_of_not_isMax (not_isMax _) _
+
+lemma Ico_succ_succ_eq_Ioc (a b : α) : Ico (succ a) (succ b) = Ioc a b :=
+  Ico_succ_succ_eq_Ioc_of_not_isMax (not_isMax _) _
+
+end SuccOrder
+
+section PredOrder
+variable [PredOrder α] {a b : α}
+
+lemma Ioc_pred_right_eq_Ioo (a b : α) : Ioc a (pred b) = Ioo a b := by
+  by_cases hb : IsMin b
+  · rw [Ioc_eq_empty (hb.mono <| pred_le _).not_lt, Ioo_eq_empty hb.not_lt]
+  · ext x
+    rw [mem_Ioc, mem_Ioo, le_pred_iff_of_not_isMin hb]
+
+lemma Icc_pred_right_eq_Ico_of_not_isMin (hb : ¬ IsMin b) (a : α) : Icc a (pred b) = Ico a b := by
+  ext x; rw [mem_Icc, mem_Ico, le_pred_iff_of_not_isMin hb]
+
+lemma Ioc_pred_left_eq_Icc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioc (pred a) b = Icc a b := by
+  ext x; rw [mem_Ioc, mem_Icc, pred_lt_iff_of_not_isMin ha]
+
+lemma Ioo_pred_left_eq_Ioc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioo (pred a) b = Ico a b := by
+  ext x; rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]
+
+lemma Ioc_pred_pred_eq_Ico_of_not_isMin (ha : ¬ IsMin a) (b : α) :
+    Ioc (pred a) (pred b) = Ico a b := by
+  rw [Ioc_pred_right_eq_Ioo, Ioo_pred_left_eq_Ioc_of_not_isMin ha]
+
+variable [NoMinOrder α]
+
+lemma Icc_pred_right_eq_Ico (a b : α) : Icc a (pred b) = Ico a b :=
+  Icc_pred_right_eq_Ico_of_not_isMin (not_isMin _) _
+
+lemma Ioc_pred_left_eq_Icc (a b : α) : Ioc (pred a) b = Icc a b :=
+  Ioc_pred_left_eq_Icc_of_not_isMin (not_isMin _) _
+
+lemma Ioo_pred_left_eq_Ioc (a b : α) : Ioo (pred a) b = Ico a b :=
+  Ioo_pred_left_eq_Ioc_of_not_isMin (not_isMin _) _
+
+lemma Ioc_pred_pred_eq_Ico (a b : α) : Ioc (pred a) (pred b) = Ico a b :=
+  Ioc_pred_pred_eq_Ico_of_not_isMin (not_isMin _) _
+
+end PredOrder
+
+section SuccPredOrder
+variable [SuccOrder α] [PredOrder α] [Nontrivial α]
+
+lemma Icc_succ_pred_eq_Ioo (a b : α) : Icc (succ a) (pred b) = Ioo a b := by
+  by_cases hb : IsMin b
+  · rw [Icc_eq_empty, Ioo_eq_empty hb.not_lt]
+    exact fun h ↦ not_isMin_succ _ <| hb.mono <| h.trans <| pred_le _
+  · rw [Icc_pred_right_eq_Ico_of_not_isMin hb, Ico_succ_left_eq_Ioo]
+
+end SuccPredOrder
+end Finset

Mathlib/Tactic.lean

@@ -234,6 +234,7 @@ import Mathlib.Tactic.Set
 import Mathlib.Tactic.SetLike
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.SimpRw
+import Mathlib.Tactic.Simproc.FinsetInterval
 import Mathlib.Tactic.Simps.Basic
 import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SplitIfs

Mathlib/Tactic/NormNum/Basic.lean

@@ -39,6 +39,9 @@ theorem IsInt.raw_refl (n : ℤ) : IsInt n n := ⟨rfl⟩
 theorem isNat_zero (α) [AddMonoidWithOne α] : IsNat (Zero.zero : α) (nat_lit 0) :=
   ⟨Nat.cast_zero.symm⟩
 
+theorem isNat_zero' (α) [AddMonoidWithOne α] : IsNat (0 : α) (nat_lit 0) :=
+  ⟨Nat.cast_zero.symm⟩
+
 /-- The `norm_num` extension which identifies the expression `Zero.zero`, returning `0`. -/
 @[norm_num Zero.zero] def evalZero : NormNumExt where eval {u α} e := do
   let sα ← inferAddMonoidWithOne α
@@ -498,6 +501,10 @@ theorem isNat_natSucc : {a : ℕ} → {a' c : ℕ} →
     IsNat a a' → Nat.succ a' = c → IsNat (a.succ) c
   | _, _,_, ⟨rfl⟩, rfl => ⟨by simp⟩
 
+theorem isNat_natPred : {a : ℕ} → {a' c : ℕ} →
+    IsNat a a' → Nat.pred a' = c → IsNat a.pred c
+  | _, _,_, ⟨rfl⟩, rfl => ⟨by simp⟩
+
 /-- The `norm_num` extension which identifies expressions of the form `Nat.succ a`,
 such that `norm_num` successfully recognises `a`. -/
 @[norm_num Nat.succ _] def evalNatSucc : NormNumExt where eval {u α} e := do