feat: cleanup on Int simp lemmas

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -1185,8 +1185,6 @@ theorem lt_tmod_of_pos (a : Int) {b : Int} (H : 0 < b) : -b < tmod a b :=
 @[simp] theorem mul_tmod_right (a b : Int) : (a * b).tmod a = 0 := by
   rw [Int.mul_comm, mul_tmod_left]
 
-attribute [local simp] Int.neg_inj
-
 theorem mul_tmod (a b n : Int) : (a * b).tmod n = (a.tmod n * b.tmod n).tmod n := by
   induction a using wlog_sign
   case inv => simp

src/Init/Data/Int/Lemmas.lean

@@ -27,16 +27,20 @@ theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat
 @[norm_cast] theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
 @[norm_cast] theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
 
-@[local simp] theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
-@[local simp] theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl
-@[local simp] theorem neg_negSucc (n : Nat) : -(-[n+1]) = succ n := rfl
+theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
+theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl
+theorem neg_negSucc (n : Nat) : -(-[n+1]) = succ n := rfl
 
 theorem negOfNat_eq : negOfNat n = -ofNat n := rfl
 
 @[simp] theorem add_def {a b : Int} : Int.add a b = a + b := rfl
 @[simp] theorem mul_def {a b : Int} : Int.mul a b = a * b := rfl
 
-/-! ## These are only for internal use -/
+/-!
+## These are only for internal use
+
+Ideally these could all be made private, but they are used in downstream libraries.
+-/
 
 @[local simp] theorem ofNat_add_ofNat (m n : Nat) : (↑m + ↑n : Int) = ↑(m + n) := rfl
 @[local simp] theorem ofNat_add_negSucc (m n : Nat) : ↑m + -[n+1] = subNatNat m (succ n) := rfl
@@ -173,8 +177,6 @@ theorem subNatNat_self : ∀ n, subNatNat n n = 0
   | 0      => rfl
   | succ m => by rw [subNatNat_of_sub_eq_zero (Nat.sub_self ..), Nat.sub_self, ofNat_zero]
 
-attribute [local simp] subNatNat_self
-
 /- # Additive group properties -/
 
 /- addition -/
@@ -230,12 +232,12 @@ protected theorem add_right_comm (a b c : Int) : a + b + c = a + c + b := by
 
 /- ## negation -/
 
-@[local simp] protected theorem add_left_neg : ∀ a : Int, -a + a = 0
+protected theorem add_left_neg : ∀ a : Int, -a + a = 0
   | 0      => rfl
-  | succ m => by simp
-  | -[m+1] => by simp
+  | succ m => by simp [neg_ofNat_succ]
+  | -[m+1] => by simp [neg_negSucc]
 
-@[local simp] protected theorem add_right_neg (a : Int) : a + -a = 0 := by
+protected theorem add_right_neg (a : Int) : a + -a = 0 := by
   rw [Int.add_comm, Int.add_left_neg]
 
 protected theorem neg_eq_of_add_eq_zero {a b : Int} (h : a + b = 0) : -a = b := by
@@ -266,7 +268,7 @@ protected theorem add_left_cancel {a b c : Int} (h : a + b = a + c) : b = c := b
   have h₁ : -a + (a + b) = -a + (a + c) := by rw [h]
   simp [← Int.add_assoc, Int.add_left_neg, Int.zero_add] at h₁; exact h₁
 
-@[local simp] protected theorem neg_add {a b : Int} : -(a + b) = -a + -b := by
+protected theorem neg_add {a b : Int} : -(a + b) = -a + -b := by
   apply Int.add_left_cancel (a := a + b)
   rw [Int.add_right_neg, Int.add_comm a, ← Int.add_assoc, Int.add_assoc b,
     Int.add_right_neg, Int.add_zero, Int.add_right_neg]
@@ -305,13 +307,13 @@ protected theorem sub_eq_zero {a b : Int} : a - b = 0 ↔ a = b :=
   ⟨Int.eq_of_sub_eq_zero, Int.sub_eq_zero_of_eq⟩
 
 protected theorem sub_sub (a b c : Int) : a - b - c = a - (b + c) := by
-  simp [Int.sub_eq_add_neg, Int.add_assoc]
+  simp [Int.sub_eq_add_neg, Int.add_assoc, Int.neg_add]
 
 protected theorem neg_sub (a b : Int) : -(a - b) = b - a := by
-  simp [Int.sub_eq_add_neg, Int.add_comm]
+  simp [Int.sub_eq_add_neg, Int.add_comm, Int.neg_add]
 
 protected theorem sub_sub_self (a b : Int) : a - (a - b) = b := by
-  simp [Int.sub_eq_add_neg, ← Int.add_assoc]
+  simp [Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_add, Int.add_right_neg]
 
 @[simp] protected theorem sub_neg (a b : Int) : a - -b = a + b := by simp [Int.sub_eq_add_neg]
 
@@ -416,11 +418,9 @@ theorem negSucc_mul_negOfNat (m n : Nat) : -[m+1] * negOfNat n = ofNat (succ m *
 theorem negOfNat_mul_negSucc (m n : Nat) : negOfNat n * -[m+1] = ofNat (n * succ m) := by
   rw [Int.mul_comm, negSucc_mul_negOfNat, Nat.mul_comm]
 
-attribute [local simp] ofNat_mul_negOfNat negOfNat_mul_ofNat
-  negSucc_mul_negOfNat negOfNat_mul_negSucc
-
 protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by
-  cases a <;> cases b <;> cases c <;> simp [Nat.mul_assoc]
+  cases a <;> cases b <;> cases c <;>
+    simp [Nat.mul_assoc, ofNat_mul_negOfNat, negOfNat_mul_ofNat, negSucc_mul_negOfNat, negOfNat_mul_negSucc]
 
 instance : Std.Associative (α := Int) (· * ·) := ⟨Int.mul_assoc⟩
 
@@ -439,7 +439,7 @@ theorem negOfNat_eq_subNatNat_zero (n) : negOfNat n = subNatNat 0 n := by cases
 theorem ofNat_mul_subNatNat (m n k : Nat) :
     m * subNatNat n k = subNatNat (m * n) (m * k) := by
   cases m with
-  | zero => simp [ofNat_zero, Int.zero_mul, Nat.zero_mul]
+  | zero => simp [ofNat_zero, Int.zero_mul, Nat.zero_mul, subNatNat_self]
   | succ m => cases n.lt_or_ge k with
     | inl h =>
       have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
@@ -467,8 +467,7 @@ theorem negSucc_mul_subNatNat (m n k : Nat) :
         Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]; rfl
     | inr h' => rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]
 
-attribute [local simp] ofNat_mul_subNatNat negOfNat_add negSucc_mul_subNatNat
-
+attribute [local simp] ofNat_mul_subNatNat negOfNat_add negSucc_mul_subNatNat in
 protected theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c
   | (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib]
   | (m:Nat), (n:Nat), -[k+1]  => by

src/Init/Data/Int/Linear.lean

@@ -1019,8 +1019,6 @@ theorem eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly)
   intro h₁ h₂
   simp [*, -Int.neg_nonpos_iff]
   replace h₂ := Int.mul_le_mul_of_nonpos_left h₂ h; simp at h₂; clear h
-  rw [← Int.neg_zero]
-  apply Int.neg_le_neg
   rw [Int.mul_comm]
   assumption
 
@@ -1081,7 +1079,6 @@ theorem eq_of_le_ge (ctx : Context) (p₁ : Poly) (p₂ : Poly)
   simp [eq_of_le_ge_cert]
   intro; subst p₂; simp [-Int.neg_nonpos_iff]
   intro h₁ h₂
-  replace h₂ := Int.neg_le_of_neg_le h₂; simp at h₂
   simp [Int.eq_iff_le_and_ge, *]
 
 def le_of_le_diseq_cert (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
@@ -1156,12 +1153,10 @@ private theorem orOver_of_exists {n p} : (∃ k, k < n ∧ p k) → OrOver n p :
 private theorem ofNat_toNat {a : Int} : a ≥ 0 → Int.ofNat a.toNat = a := by cases a <;> simp
 private theorem cast_toNat {a : Int} : a ≥ 0 → a.toNat = a := by cases a <;> simp
 private theorem ofNat_lt {a : Int} {n : Nat} : a ≥ 0 → a < Int.ofNat n → a.toNat < n := by cases a <;> simp
-@[local simp] private theorem lcm_neg_left (a b : Int) : Int.lcm (-a) b = Int.lcm a b := by simp [Int.lcm]
-@[local simp] private theorem lcm_neg_right (a b : Int) : Int.lcm a (-b) = Int.lcm a b := by simp [Int.lcm]
-@[local simp] private theorem gcd_neg_left (a b : Int) : Int.gcd (-a) b = Int.gcd a b := by simp [Int.gcd]
-@[local simp] private theorem gcd_neg_right (a b : Int) : Int.gcd a (-b) = Int.gcd a b := by simp [Int.gcd]
-@[local simp] private theorem gcd_zero (a : Int) : Int.gcd a 0 = a.natAbs := by simp [Int.gcd]
-@[local simp] private theorem lcm_one (a : Int) : Int.lcm a 1 = a.natAbs := by simp [Int.lcm]
+private theorem lcm_neg_left (a b : Int) : Int.lcm (-a) b = Int.lcm a b := by simp [Int.lcm]
+private theorem lcm_neg_right (a b : Int) : Int.lcm a (-b) = Int.lcm a b := by simp [Int.lcm]
+private theorem gcd_zero (a : Int) : Int.gcd a 0 = a.natAbs := by simp [Int.gcd]
+private theorem lcm_one (a : Int) : Int.lcm a 1 = a.natAbs := by simp [Int.lcm]
 
 private theorem cooper_dvd_left_core
     {a b c d s p q x : Int} (a_neg : a < 0) (b_pos : 0 < b) (d_pos : 0 < d)

src/Init/Data/Int/OfNat.lean

@@ -43,9 +43,6 @@ def Expr.denoteAsInt (ctx : Context) : Expr → Int
   | .div a b  => Int.ediv (denoteAsInt ctx a) (denoteAsInt ctx b)
   | .mod a b  => Int.emod (denoteAsInt ctx a) (denoteAsInt ctx b)
 
-@[local simp] private theorem fold_div (a b : Nat) : a.div b = a / b := rfl
-@[local simp] private theorem fold_mod (a b : Nat) : a.mod b = a % b := rfl
-
 theorem Expr.denoteAsInt_eq (ctx : Context) (e : Expr) : e.denoteAsInt ctx = e.denote ctx := by
   induction e <;> simp [denote, denoteAsInt, Int.ofNat_ediv, *] <;> rfl
 

src/Init/Data/Int/Order.lean

@@ -33,20 +33,18 @@ theorem lt_iff_add_one_le {a b : Int} : a < b ↔ a + 1 ≤ b := .rfl
 theorem le.intro_sub {a b : Int} (n : Nat) (h : b - a = n) : a ≤ b := by
   simp [le_def, h]; constructor
 
-attribute [local simp] Int.add_left_neg Int.add_right_neg Int.neg_add
-
 theorem le.intro {a b : Int} (n : Nat) (h : a + n = b) : a ≤ b :=
-  le.intro_sub n <| by rw [← h, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc]
+  le.intro_sub n <| by rw [← h, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc, Int.add_right_neg]
 
 theorem le.dest_sub {a b : Int} (h : a ≤ b) : ∃ n : Nat, b - a = n := nonneg_def.1 h
 
 theorem le.dest {a b : Int} (h : a ≤ b) : ∃ n : Nat, a + n = b :=
   let ⟨n, h₁⟩ := le.dest_sub h
-  ⟨n, by rw [← h₁, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc]⟩
+  ⟨n, by rw [← h₁, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_neg]⟩
 
 protected theorem le_total (a b : Int) : a ≤ b ∨ b ≤ a :=
   (nonneg_or_nonneg_neg (b - a)).imp_right fun H => by
-    rwa [show -(b - a) = a - b by simp [Int.add_comm, Int.sub_eq_add_neg]] at H
+    rwa [show -(b - a) = a - b by simp [Int.neg_add,Int.add_comm, Int.sub_eq_add_neg]] at H
 
 @[simp, norm_cast] theorem ofNat_le {m n : Nat} : (↑m : Int) ≤ ↑n ↔ m ≤ n :=
   ⟨fun h =>
@@ -198,7 +196,7 @@ theorem le_natAbs {a : Int} : a ≤ natAbs a :=
   | .inl h => by rw [eq_natAbs_of_nonneg h]; apply Int.le_refl
   | .inr h => Int.le_trans h (ofNat_zero_le _)
 
-theorem negSucc_lt_zero (n : Nat) : -[n+1] < 0 :=
+@[simp] theorem negSucc_lt_zero (n : Nat) : -[n+1] < 0 :=
   Int.not_le.1 fun h => let ⟨_, h⟩ := eq_ofNat_of_zero_le h; nomatch h
 
 theorem negSucc_le_zero (n : Nat) : -[n+1] ≤ 0 :=
@@ -253,6 +251,12 @@ protected theorem neg_le_neg {a b : Int} (h : a ≤ b) : -b ≤ -a := by
 @[simp] protected theorem neg_le_neg_iff {a b : Int} : -a ≤ -b ↔ b ≤ a :=
   ⟨fun h => by simpa using Int.neg_le_neg h, Int.neg_le_neg⟩
 
+@[simp] protected theorem neg_le_zero_iff {a : Int} : -a ≤ 0 ↔ 0 ≤ a := by
+  rw [← Int.neg_zero, Int.neg_le_neg_iff, Int.neg_zero]
+
+@[simp] protected theorem zero_le_neg_iff {a : Int} : 0 ≤ -a ↔ a ≤ 0 := by
+  rw [← Int.neg_zero, Int.neg_le_neg_iff, Int.neg_zero]
+
 protected theorem le_of_neg_le_neg {a b : Int} (h : -b ≤ -a) : a ≤ b :=
   suffices - -a ≤ - -b by simp [Int.neg_neg] at this; assumption
   Int.neg_le_neg h
@@ -270,6 +274,15 @@ protected theorem neg_lt_neg {a b : Int} (h : a < b) : -b < -a := by
   have : 0 + -b < -a + b + -b := Int.add_lt_add_right this (-b)
   rwa [Int.add_neg_cancel_right, Int.zero_add] at this
 
+@[simp] protected theorem neg_lt_neg_iff {a b : Int} : -a < -b ↔ b < a :=
+  ⟨fun h => by simpa using Int.neg_lt_neg h, Int.neg_lt_neg⟩
+
+@[simp] protected theorem neg_lt_zero_iff {a : Int} : -a < 0 ↔ 0 < a := by
+  rw [← Int.neg_zero, Int.neg_lt_neg_iff, Int.neg_zero]
+
+@[simp] protected theorem zero_lt_neg_iff {a : Int} : 0 < -a ↔ a < 0 := by
+  rw [← Int.neg_zero, Int.neg_lt_neg_iff, Int.neg_zero]
+
 protected theorem neg_neg_of_pos {a : Int} (h : 0 < a) : -a < 0 := by
   have : -a < -0 := Int.neg_lt_neg h
   rwa [Int.neg_zero] at this
@@ -568,8 +581,8 @@ theorem toNat_of_nonneg {a : Int} (h : 0 ≤ a) : (toNat a : Int) = a := by
 
 @[simp] theorem ofNat_toNat (a : Int) : (a.toNat : Int) = max a 0 := by
   match a with
-  | Int.ofNat n => simp
-  | Int.negSucc n => simp
+  | (n : Nat) => simp
+  | -(n + 1 : Nat) => norm_cast
 
 theorem self_le_toNat (a : Int) : a ≤ toNat a := by rw [toNat_eq_max]; apply Int.le_max_left
 
@@ -1123,8 +1136,8 @@ theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
 @[simp] theorem sign_pos_iff : 0 < sign x ↔ 0 < x := by
   match x with
   | 0
-  | .ofNat (_ + 1)
-  | .negSucc _ => simp
+  | .ofNat (_ + 1) => simp
+  | .negSucc x => simp
 
 @[simp] theorem sign_nonpos_iff : sign x ≤ 0 ↔ x ≤ 0 := by
   match x with
@@ -1136,7 +1149,7 @@ theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
   match x with
   | 0 => simp
   | .ofNat (_ + 1) => simpa using le.intro_sub _ rfl
-  | .negSucc _ => simpa using negSucc_lt_zero _
+  | .negSucc _ => simp
 
 @[simp] theorem mul_sign_self : ∀ i : Int, i * sign i = natAbs i
   | succ _ => Int.mul_one _