From 9022a7ddb9c3283b8c37e8f889da80b87bc55840 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 14 Sep 2023 09:08:49 +0000 Subject: [PATCH] chore: reduce use of Init.Data.Int.CompLemmas (#7142) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 --- Mathlib/NumberTheory/LegendreSymbol/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/LegendreSymbol/Basic.lean b/Mathlib/NumberTheory/LegendreSymbol/Basic.lean index a1a64044be2df..7ba216590aa2a 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/Basic.lean +++ b/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