fix(data/int/basic,category_theory/equivalence): use neg not minus in…

… lemma names (#6384)




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/group_power/lemmas.lean

@@ -717,7 +717,7 @@ by induction b; simp [*, mul_add, pow_succ, add_comm]
 @[simp] lemma int.to_add_gpow (a : multiplicative ℤ) (b : ℤ) : to_add (a ^ b) = to_add a * b :=
 int.induction_on b (by simp)
   (by simp [gpow_add, mul_add] {contextual := tt})
-  (by simp [gpow_add, mul_add, sub_eq_add_neg, -int.add_minus_one] {contextual := tt})
+  (by simp [gpow_add, mul_add, sub_eq_add_neg, -int.add_neg_one] {contextual := tt})
 
 @[simp] lemma int.of_add_mul (a b : ℤ) : of_add (a * b) = of_add a ^ b :=
 (int.to_add_gpow _ _).symm

src/category_theory/equivalence.lean

@@ -367,7 +367,7 @@ instance : has_pow (C ≌ C) ℤ := ⟨pow⟩
 
 @[simp] lemma pow_zero (e : C ≌ C) : e^(0 : ℤ) = equivalence.refl := rfl
 @[simp] lemma pow_one (e : C ≌ C) : e^(1 : ℤ) = e := rfl
-@[simp] lemma pow_minus_one (e : C ≌ C) : e^(-1 : ℤ) = e.symm := rfl
+@[simp] lemma pow_neg_one (e : C ≌ C) : e^(-1 : ℤ) = e.symm := rfl
 
 -- TODO as necessary, add the natural isomorphisms `(e^a).trans e^b ≅ e^(a+b)`.
 -- At this point, we haven't even defined the category of equivalences.

src/data/int/basic.lean

@@ -60,7 +60,7 @@ instance : linear_ordered_comm_ring int :=
 instance : linear_ordered_add_comm_group int :=
 by apply_instance
 
-@[simp] lemma add_minus_one (i : ℤ) : i + -1 = i - 1 := rfl
+@[simp] lemma add_neg_one (i : ℤ) : i + -1 = i - 1 := rfl
 
 theorem abs_eq_nat_abs : ∀ a : ℤ, abs a = nat_abs a
 | (n : ℕ) := abs_of_nonneg $ coe_zero_le _

src/data/num/lemmas.lean

@@ -822,7 +822,7 @@ begin
   conv { to_lhs, rw ← zneg_zneg n },
   rw [← zneg_bit1, cast_zneg, cast_bit1],
   have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ), {simp [add_comm, add_left_comm]},
-  simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg, -int.add_minus_one]
+  simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg, -int.add_neg_one]
 end
 
 theorem add_zero (n : znum) : n + 0 = n := by cases n; refl
@@ -843,7 +843,7 @@ theorem cast_to_znum : ∀ n : pos_num, (n : znum) = znum.pos n
 | (bit0 p) := (znum.bit0_of_bit0 p).trans $ congr_arg _ (cast_to_znum p)
 | (bit1 p) := (znum.bit1_of_bit1 p).trans $ congr_arg _ (cast_to_znum p)
 
-local attribute [-simp] int.add_minus_one
+local attribute [-simp] int.add_neg_one
 
 theorem cast_sub' [add_group α] [has_one α] : ∀ m n : pos_num, (sub' m n : α) = m - n
 | a        1        := by rw [sub'_one, num.cast_to_znum,

src/group_theory/free_group.lean

@@ -633,7 +633,7 @@ def free_group_unit_equiv_int : free_group unit ≃ ℤ :=
   right_inv :=
     λ x, int.induction_on x (by simp)
     (λ i ih, by simp at ih; simp [gpow_add, ih])
-    (λ i ih, by simp at ih; simp [gpow_add, ih, sub_eq_add_neg, -int.add_minus_one])
+    (λ i ih, by simp at ih; simp [gpow_add, ih, sub_eq_add_neg, -int.add_neg_one])
 }
 
 section category