feat(*): make int.nonneg irreducible (#4601)

In #4474, `int.lt` was made irreducible. We make `int.nonneg` irreducible, which is stronger as `int.lt` is expressed in terms of `int.nonneg`.

Author: sgouezel

src/algebra/field_power.lean

@@ -90,7 +90,7 @@ lemma one_lt_pow {K} [linear_ordered_semiring K] {p : K} (hp : 1 < p) : ∀ {n :
   end
 
 section
-local attribute [semireducible] int.lt
+local attribute [semireducible] int.nonneg
 lemma one_lt_fpow {K}  [discrete_linear_ordered_field K] {p : K} (hp : 1 < p) :
   ∀ z : ℤ, 0 < z → 1 < p ^ z
 | (int.of_nat n) h := one_lt_pow hp (nat.succ_le_of_lt (int.lt_of_coe_nat_lt_coe_nat h))

src/data/int/basic.lean

@@ -1238,4 +1238,4 @@ end classical
 
 end int
 
-attribute [irreducible] int.lt
+attribute [irreducible] int.nonneg

src/data/int/range.lean

@@ -8,6 +8,8 @@ import data.list.range
 
 namespace int
 
+local attribute [semireducible] int.nonneg
+
 /-- List enumerating `[m, n)`. -/
 def range (m n : ℤ) : list ℤ :=
 (list.range (to_nat (n-m))).map $ λ r, m+r
@@ -32,8 +34,6 @@ instance decidable_le_le (P : int → Prop) [decidable_pred P] (m n : ℤ) :
   decidable (∀ r, m ≤ r → r ≤ n → P r) :=
 decidable_of_iff (∀ r ∈ range m (n+1), P r) $ by simp only [mem_range_iff, and_imp, lt_add_one_iff]
 
-local attribute [semireducible] int.lt
-
 instance decidable_lt_lt (P : int → Prop) [decidable_pred P] (m n : ℤ) :
   decidable (∀ r, m < r → r < n → P r) :=
 int.decidable_le_lt P _ _

src/data/int/sqrt.lean

@@ -22,6 +22,6 @@ theorem exists_mul_self (x : ℤ) :
 ⟨λ ⟨n, hn⟩, by rw [← hn, sqrt_eq, ← int.coe_nat_mul, nat_abs_mul_self],
 λ h, ⟨sqrt x, h⟩⟩
 
-theorem sqrt_nonneg (n : ℤ) : 0 ≤ sqrt n := trivial
+theorem sqrt_nonneg (n : ℤ) : 0 ≤ sqrt n := coe_nat_nonneg _
 
 end int

src/data/nat/modeq.lean

@@ -96,6 +96,8 @@ by rw [modeq_iff_dvd] at *; exact dvd.trans (dvd_mul_left (n : ℤ) (m : ℤ)) h
 theorem modeq_of_modeq_mul_right (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n] :=
 mul_comm m n ▸ modeq_of_modeq_mul_left _
 
+local attribute [semireducible] int.nonneg
+
 /-- The natural number less than `n*m` congruent to `a` mod `n` and `b` mod `m` -/
 def chinese_remainder (co : coprime n m) (a b : ℕ) : {k // k ≡ a [MOD n] ∧ k ≡ b [MOD m]} :=
 ⟨let (c, d) := xgcd n m in int.to_nat ((b * c * n + a * d * m) % (n * m)), begin

src/data/rat/sqrt.lean

@@ -27,6 +27,7 @@ theorem exists_mul_self (x : ℚ) : (∃ q, q * q = x) ↔ rat.sqrt x * rat.sqrt
 
 theorem sqrt_nonneg (q : ℚ) : 0 ≤ rat.sqrt q :=
 nonneg_iff_zero_le.1 $ (mk_nonneg _ $ int.coe_nat_pos.2 $
-nat.pos_of_ne_zero $ λ H, nat.pos_iff_ne_zero.1 q.pos $ nat.sqrt_eq_zero.1 H).2 trivial
+nat.pos_of_ne_zero $ λ H, nat.pos_iff_ne_zero.1 q.pos $ nat.sqrt_eq_zero.1 H).2
+$ int.coe_nat_nonneg _
 
 end rat

src/data/zmod/basic.lean

@@ -428,6 +428,8 @@ begin
   apply int.modeq.mod_modeq,
 end
 
+local attribute [semireducible] int.nonneg
+
 @[simp] lemma coe_to_nat (p : ℕ) :
   ∀ {z : ℤ} (h : 0 ≤ z), (z.to_nat : zmod p) = z
 | (n : ℕ) h := by simp only [int.cast_coe_nat, int.to_nat_coe_nat]

src/data/zsqrtd/gaussian_int.lean

@@ -90,7 +90,7 @@ by rw [norm, norm_sq]; simp
 @[simp] lemma nat_cast_complex_norm (x : ℤ[i]) : (x.norm : ℂ) = (x : ℂ).norm_sq :=
 by cases x; rw [norm, norm_sq]; simp
 
-lemma norm_nonneg (x : ℤ[i]) : 0 ≤ norm x := norm_nonneg trivial _
+lemma norm_nonneg (x : ℤ[i]) : 0 ≤ norm x := norm_nonneg (by norm_num) _
 
 @[simp] lemma norm_eq_zero {x : ℤ[i]} : norm x = 0 ↔ x = 0 :=
 by rw [← @int.cast_inj ℝ _ _ _]; simp

src/number_theory/lucas_lehmer.lean

@@ -93,7 +93,7 @@ end
 lemma s_mod_nonneg (p : ℕ) (w : 0 < p) (i : ℕ) : 0 ≤ s_mod p i :=
 begin
   cases i; dsimp [s_mod],
-  { trivial, },
+  { exact sup_eq_left.mp rfl },
   { apply int.mod_nonneg, exact mersenne_int_ne_zero p w },
 end
 

src/tactic/omega/eq_elim.lean

@@ -25,7 +25,7 @@ if (2 * (i % j)) < j
 then i % j
 else (i % j) - j
 
-local attribute [semireducible] int.lt
+local attribute [semireducible] int.nonneg
 lemma symmod_add_one_self {i : int} :
   0 < i → symmod i (i+1) = -1 :=
 begin