feat: add lemmas about Int ranges (#11705)

This PR provides many lemmas about `Int` ranges, in analogy to those
about `Nat` ranges. A few necessary basic `Int` lemmas are added. The PR
also removes `simp` annotations on `Rcc.toList_eq_toList_rco`,
`Nat.toList_rcc_eq_toList_rco` and consorts.

src/Init/Data/Int/Lemmas.lean

@@ -333,6 +333,12 @@ protected theorem sub_sub_self (a b : Int) : a - (a - b) = b := by
 @[simp] protected theorem add_sub_cancel (a b : Int) : a + b - b = a :=
   Int.add_neg_cancel_right a b
 
+protected theorem add_sub_add_right (n k m : Int) : (n + k) - (m + k) = n - m := by
+  rw [Int.add_comm m, ← Int.sub_sub, Int.add_sub_cancel]
+
+protected theorem add_sub_add_left (k n m : Int) : (k + n) - (k + m) = n - m := by
+  rw [Int.add_comm k, Int.add_comm k, Int.add_sub_add_right]
+
 protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
   rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_neg_eq_sub]
 

src/Init/Data/Int/Order.lean

@@ -474,6 +474,20 @@ protected theorem max_lt {a b c : Int} : max a b < c ↔ a < c ∧ b < c := by
   simp only [Int.lt_iff_add_one_le]
   simpa using Int.max_le (a := a + 1) (b := b + 1) (c := c)
 
+protected theorem max_eq_right_iff {a b : Int} : max a b = b ↔ a ≤ b := by
+  apply Iff.intro
+  · intro h
+    rw [← h]
+    apply Int.le_max_left
+  · apply Int.max_eq_right
+
+protected theorem max_eq_left_iff {a b : Int} : max a b = a ↔ b ≤ a := by
+  apply Iff.intro
+  · intro h
+    rw [← h]
+    apply Int.le_max_right
+  · apply Int.max_eq_left
+
 @[simp] theorem ofNat_max_zero (n : Nat) : (max (n : Int) 0) = n := by
   rw [Int.max_eq_left (natCast_nonneg n)]
 
@@ -912,6 +926,16 @@ protected theorem sub_right_le_of_le_add {a b c : Int} (h : a ≤ b + c) : a - c
   have h := Int.add_le_add_right h (-c)
   rwa [Int.add_neg_cancel_right] at h
 
+protected theorem sub_right_le_iff_le_add {a b c : Int} : a - c ≤ b ↔ a ≤ b + c :=
+  ⟨Int.le_add_of_sub_right_le, Int.sub_right_le_of_le_add⟩
+
+theorem toNat_sub_eq_zero_iff (m n : Int) : toNat (m - n) = 0 ↔ m ≤ n := by
+  rw [← ofNat_inj, ofNat_toNat, cast_ofNat_Int, Int.max_eq_right_iff, Int.sub_right_le_iff_le_add,
+    Int.zero_add]
+
+theorem zero_eq_toNat_sub_iff (m n : Int) : 0 = toNat (m - n) ↔ m ≤ n := by
+  rw [eq_comm (a := 0), toNat_sub_eq_zero_iff]
+
 protected theorem le_add_of_neg_add_le_left {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c := by
   rw [Int.add_comm] at h
   exact Int.le_add_of_sub_left_le h
@@ -989,6 +1013,10 @@ protected theorem lt_sub_right_of_add_lt {a b c : Int} (h : a + b < c) : a < c -
   have h := Int.add_lt_add_right h (-b)
   rwa [Int.add_neg_cancel_right] at h
 
+protected theorem lt_sub_right_iff_add_lt {a b c : Int} :
+    a < c - b ↔ a + b < c :=
+  ⟨Int.add_lt_of_lt_sub_right, Int.lt_sub_right_of_add_lt⟩
+
 protected theorem lt_add_of_neg_add_lt {a b c : Int} (h : -b + a < c) : a < b + c := by
   have h := Int.add_lt_add_left h b
   rwa [Int.add_neg_cancel_left] at h

src/Init/Data/Range/Polymorphic/Lemmas.lean

@@ -586,7 +586,6 @@ public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
         [] := by
   rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl
 
-@[simp]
 public theorem toList_eq_toList_rco [LE α] [DecidableLE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
@@ -1300,7 +1299,6 @@ public theorem toArray_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable
   simp only [← Internal.toList_eq_toList_iter, toList_eq_match_rcc]
   split <;> simp
 
-@[simp]
 public theorem toList_eq_toList_roo [LE α] [DecidableLE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]