chore: reduce use of Init.Data.Int.CompLemmas (#7142)

`Mathlib.Init.Data.Int.CompLemmas` was ported from core, and was never really intended for outside use. Nevertheless, people started using it. (Surprise!)

This PR removes one out of the two uses in Mathlib.

If anyone would like to do the other in a separate PR, please do! You would need to reprove
```
theorem natAbs_add_nonneg {a b : ℤ} (wa : 0 ≤ a) (wb : 0 ≤ b) :
    Int.natAbs (a + b) = Int.natAbs a + Int.natAbs b := sorry

theorem natAbs_add_neg {a b : ℤ} (wa : a < 0) (wb : b < 0) :
    Int.natAbs (a + b) = Int.natAbs a + Int.natAbs b := sorry
```



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

Mathlib/NumberTheory/LegendreSymbol/Basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Michael Stoll
 -/
-import Mathlib.Init.Data.Int.CompLemmas
 import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
 
 #align_import number_theory.legendre_symbol.basic from "leanprover-community/mathlib"@"5b2fe80501ff327b9109fb09b7cc8c325cd0d7d9"
@@ -255,7 +254,7 @@ theorem eq_zero_mod_of_eq_neg_one {p : ℕ} [Fact p.Prime] {a : ℤ} (h : legend
   have ha : (a : ZMod p) ≠ 0 := by
     intro hf
     rw [(eq_zero_iff p a).mpr hf] at h
-    exact Int.zero_ne_neg_of_ne zero_ne_one h
+    simp at h
   by_contra hf
   cases' imp_iff_or_not.mp (not_and'.mp hf) with hx hy
   · rw [eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy, eq_neg_self_iff] at h