chore(data/int/order/basic): Fix lemma name (#17967)

`int.coe_nat_abs` wasn't referring to the correct lemma. Change the name, add the lemma it should correspond to and tag both with `simp` and `norm_cast`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

archive/imo/imo2013_q5.lean

@@ -103,7 +103,7 @@ begin
       ... = ((q.num.nat_abs : ℤ) : ℝ) : congr_arg coe (int.nat_abs_of_nonneg num_pos.le).symm
       ... ≤ f q.num.nat_abs           : H4 q.num.nat_abs
                                           (int.nat_abs_pos_of_ne_zero num_pos.ne')
-      ... = f q.num : by { rw ←int.nat_abs_of_nonneg num_pos.le, norm_cast }
+      ... = f q.num : by rw [nat.cast_nat_abs, abs_of_nonneg num_pos.le]
       ... = f (q * q.denom) : by rw ←rat.mul_denom_eq_num
       ... ≤ f q * f q.denom : H1 q q.denom hq (nat.cast_pos.mpr q.pos),
   have h_f_denom_pos :=

src/algebra/euclidean_domain/instances.lean

@@ -33,7 +33,7 @@ instance int.euclidean_domain : euclidean_domain ℤ :=
   r := λ a b, a.nat_abs < b.nat_abs,
   r_well_founded := measure_wf (λ a, int.nat_abs a),
   remainder_lt := λ a b b0, int.coe_nat_lt.1 $
-    by { rw [int.nat_abs_of_nonneg (int.mod_nonneg _ b0), ← int.abs_eq_nat_abs],
+    by { rw [int.nat_abs_of_nonneg (int.mod_nonneg _ b0), int.coe_nat_abs],
       exact int.mod_lt _ b0 },
   mul_left_not_lt := λ a b b0, not_lt_of_ge $
     by {rw [← mul_one a.nat_abs, int.nat_abs_mul],

src/algebra/group_power/lemmas.lean

@@ -300,9 +300,9 @@ lemma abs_zsmul (n : ℤ) (a : α) : |n • a| = |n| • |a| :=
 begin
   obtain n0 | n0 := le_total 0 n,
   { lift n to ℕ using n0,
-    simp only [abs_nsmul, coe_nat_abs, coe_nat_zsmul] },
+    simp only [abs_nsmul, abs_coe_nat, coe_nat_zsmul] },
   { lift (- n) to ℕ using neg_nonneg.2 n0 with m h,
-    rw [← abs_neg (n • a), ← neg_zsmul, ← abs_neg n, ← h, coe_nat_zsmul, coe_nat_abs,
+    rw [← abs_neg (n • a), ← neg_zsmul, ← abs_neg n, ← h, coe_nat_zsmul, abs_coe_nat,
       coe_nat_zsmul],
     exact abs_nsmul m _ },
 end
@@ -524,8 +524,7 @@ end linear_ordered_ring
 
 namespace int
 
-@[simp] lemma nat_abs_sq (x : ℤ) : (x.nat_abs ^ 2 : ℤ) = x ^ 2 :=
-by rw [sq, int.nat_abs_mul_self', sq]
+lemma nat_abs_sq (x : ℤ) : (x.nat_abs ^ 2 : ℤ) = x ^ 2 := by rw [sq, int.nat_abs_mul_self', sq]
 
 alias nat_abs_sq ← nat_abs_pow_two
 

src/analysis/normed/field/basic.lean

@@ -699,7 +699,7 @@ lemma int.norm_eq_abs (n : ℤ) : ‖n‖ = |n| := rfl
 lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = ‖n‖₊ :=
 nnreal.eq $ calc ((n.nat_abs : ℝ≥0) : ℝ)
                = (n.nat_abs : ℤ) : by simp only [int.cast_coe_nat, nnreal.coe_nat_cast]
-           ... = |n|           : by simp only [← int.abs_eq_nat_abs, int.cast_abs]
+           ... = |n|           : by simp only [int.coe_nat_abs, int.cast_abs]
            ... = ‖n‖              : rfl
 
 lemma int.abs_le_floor_nnreal_iff (z : ℤ) (c : ℝ≥0) : |z| ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c :=

src/data/int/basic.lean

@@ -181,7 +181,7 @@ end
 
 variables {a b : ℤ} {n : ℕ}
 
-attribute [simp] nat_abs nat_abs_of_nat nat_abs_zero nat_abs_one
+attribute [simp] nat_abs_of_nat nat_abs_zero nat_abs_one
 
 theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b :=
 begin
@@ -212,7 +212,7 @@ lemma nat_abs_mul_nat_abs_eq {a b : ℤ} {c : ℕ} (h : a * b = (c : ℤ)) :
   a.nat_abs * b.nat_abs = c :=
 by rw [← nat_abs_mul, h, nat_abs_of_nat]
 
-@[simp] lemma nat_abs_mul_self' (a : ℤ) : (nat_abs a * nat_abs a : ℤ) = a * a :=
+lemma nat_abs_mul_self' (a : ℤ) : (nat_abs a * nat_abs a : ℤ) = a * a :=
 by rw [← int.coe_nat_mul, nat_abs_mul_self]
 
 theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 :=

src/data/int/dvd/basic.lean

@@ -27,10 +27,10 @@ namespace int
  λ ⟨k, e⟩, dvd.intro k $ by rw [e, int.coe_nat_mul]⟩
 
 theorem coe_nat_dvd_left {n : ℕ} {z : ℤ} : (↑n : ℤ) ∣ z ↔ n ∣ z.nat_abs :=
-by rcases nat_abs_eq z with eq | eq; rw eq; simp [coe_nat_dvd]
+by rcases nat_abs_eq z with eq | eq; rw eq; simp [←coe_nat_dvd]
 
 theorem coe_nat_dvd_right {n : ℕ} {z : ℤ} : z ∣ (↑n : ℤ) ↔ z.nat_abs ∣ n :=
-by rcases nat_abs_eq z with eq | eq; rw eq; simp [coe_nat_dvd]
+by rcases nat_abs_eq z with eq | eq; rw eq; simp [←coe_nat_dvd]
 
 theorem le_of_dvd {a b : ℤ} (bpos : 0 < b) (H : a ∣ b) : a ≤ b :=
 match a, b, eq_succ_of_zero_lt bpos, H with

src/data/int/order/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 import data.int.basic
+import data.int.cast.basic
 import algebra.ring.divisibility
 import algebra.order.group.abs
 import algebra.order.ring.char_zero
@@ -54,6 +55,11 @@ theorem abs_eq_nat_abs : ∀ a : ℤ, |a| = nat_abs a
 | (n : ℕ) := abs_of_nonneg $ coe_zero_le _
 | -[1+ n] := abs_of_nonpos $ le_of_lt $ neg_succ_lt_zero _
 
+@[simp, norm_cast] lemma coe_nat_abs (n : ℤ) : (n.nat_abs : ℤ) = |n| := n.abs_eq_nat_abs.symm
+
+lemma _root_.nat.cast_nat_abs {α : Type*} [add_group_with_one α] (n : ℤ) : (n.nat_abs : α) = ↑|n| :=
+by rw [←int.coe_nat_abs, int.cast_coe_nat]
+
 theorem nat_abs_abs (a : ℤ) : nat_abs (|a|) = nat_abs a :=
 by rw [abs_eq_nat_abs]; refl
 
@@ -68,8 +74,7 @@ lemma coe_nat_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n :=
 ⟨λ h, nat.pos_of_ne_zero (coe_nat_ne_zero.1 h),
 λ h, (ne_of_lt (coe_nat_lt.2 h)).symm⟩
 
-theorem coe_nat_abs (n : ℕ) : |(n : ℤ)| = n :=
-abs_of_nonneg (coe_nat_nonneg n)
+@[norm_cast] lemma abs_coe_nat (n : ℕ) : |(n : ℤ)| = n := abs_of_nonneg (coe_nat_nonneg n)
 
 /-! ### succ and pred -/
 

src/data/rat/floor.lean

@@ -126,9 +126,8 @@ begin
     have : ((q.denom - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.denom - q.num * ⌊q_inv⌋, by
     { suffices : ((q.denom : ℤ) - q.num * ⌊q_inv⌋).nat_abs.coprime q.num.nat_abs, by
         exact_mod_cast (rat.num_div_eq_of_coprime q_num_pos this),
-      have : (q.num.nat_abs : ℚ) = (q.num : ℚ), by exact_mod_cast q_num_abs_eq_q_num,
       have tmp := nat.coprime_sub_mul_floor_rat_div_of_coprime q.cop.symm,
-      simpa only [this, q_num_abs_eq_q_num] using tmp },
+      simpa only [nat.cast_nat_abs, abs_of_nonneg q_num_pos.le] using tmp },
     rwa this },
   -- to show the claim, start with the following inequality
   have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.denom < q⁻¹.denom, by

src/data/sign.lean

@@ -379,7 +379,7 @@ begin
     λ a, a.1, λ a, a.1.prop, _, _⟩,
   { simp [@sum_attach _ _ _ _ (λ a, (f a).nat_abs)] },
   { intros x hx,
-    simp [sum_sigma, hx, ← int.sign_eq_sign, int.sign_mul_nat_abs, mul_comm ((f _).nat_abs : ℤ),
+    simp [sum_sigma, hx, ← int.sign_eq_sign, int.sign_mul_abs, mul_comm (|f _|),
       @sum_attach _ _ _ _ (λ a, ∑ j in range (f a).nat_abs, if a = x then (f a).sign else 0)] }
 end
 

src/dynamics/ergodic/add_circle.lean

@@ -102,7 +102,7 @@ lemma ergodic_zsmul {n : ℤ} (hn : 1 < |n|) : ergodic (λ (y : add_circle T), n
     have hu₀ : ∀ j, add_order_of (u j) = n.nat_abs^j,
     { exact λ j, add_order_of_div_of_gcd_eq_one (pow_pos (pos_of_gt hn) j) (gcd_one_left _), },
     have hnu : ∀ j, n^j • (u j) = 0 := λ j, by rw [← add_order_of_dvd_iff_zsmul_eq_zero, hu₀,
-      int.coe_nat_pow, ← int.abs_eq_nat_abs, ← abs_pow, abs_dvd],
+      int.coe_nat_pow, int.coe_nat_abs, ← abs_pow, abs_dvd],
     have hu₁ : ∀ j, ((u j) +ᵥ s : set _) =ᵐ[volume] s :=
       λ j, by rw vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j),
     have hu₂ : tendsto (λ j, add_order_of $ u j) at_top at_top,

src/number_theory/zsqrtd/gaussian_int.lean

@@ -96,12 +96,12 @@ by rw [← @int.cast_inj ℝ _ _ _]; simp
 lemma norm_pos {x : ℤ[i]} : 0 < norm x ↔ x ≠ 0 :=
 by rw [lt_iff_le_and_ne, ne.def, eq_comm, norm_eq_zero]; simp [norm_nonneg]
 
-lemma coe_nat_abs_norm (x : ℤ[i]) : (x.norm.nat_abs : ℤ) = x.norm :=
+lemma abs_coe_nat_norm (x : ℤ[i]) : (x.norm.nat_abs : ℤ) = x.norm :=
 int.nat_abs_of_nonneg (norm_nonneg _)
 
 @[simp] lemma nat_cast_nat_abs_norm {α : Type*} [ring α]
   (x : ℤ[i]) : (x.norm.nat_abs : α) = x.norm :=
-by rw [← int.cast_coe_nat, coe_nat_abs_norm]
+by rw [← int.cast_coe_nat, abs_coe_nat_norm]
 
 lemma nat_abs_norm_eq (x : ℤ[i]) : x.norm.nat_abs =
   x.re.nat_abs * x.re.nat_abs + x.im.nat_abs * x.im.nat_abs :=
@@ -169,7 +169,7 @@ lemma norm_le_norm_mul_left (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) :
   (norm x).nat_abs ≤ (norm (x * y)).nat_abs :=
 by rw [zsqrtd.norm_mul, int.nat_abs_mul];
   exact le_mul_of_one_le_right (nat.zero_le _)
-    (int.coe_nat_le.1 (by rw [coe_nat_abs_norm]; exact int.add_one_le_of_lt (norm_pos.2 hy)))
+    (int.coe_nat_le.1 (by rw [abs_coe_nat_norm]; exact int.add_one_le_of_lt (norm_pos.2 hy)))
 
 instance : nontrivial ℤ[i] :=
 ⟨⟨0, 1, dec_trivial⟩⟩

src/ring_theory/int/basic.lean

@@ -91,24 +91,22 @@ instance : normalization_monoid ℤ :=
 lemma normalize_of_nonneg {z : ℤ} (h : 0 ≤ z) : normalize z = z :=
 show z * ↑(ite _ _ _) = z, by rw [if_pos h, units.coe_one, mul_one]
 
-lemma normalize_of_neg {z : ℤ} (h : z < 0) : normalize z = -z :=
-show z * ↑(ite _ _ _) = -z,
-by rw [if_neg (not_le_of_gt h), units.coe_neg, units.coe_one, mul_neg_one]
+lemma normalize_of_nonpos {z : ℤ} (h : z ≤ 0) : normalize z = -z :=
+begin
+  obtain rfl | h := h.eq_or_lt,
+  { simp },
+  { change z * ↑(ite _ _ _) = -z,
+   rw [if_neg (not_le_of_gt h), units.coe_neg, units.coe_one, mul_neg_one] }
+end
 
 lemma normalize_coe_nat (n : ℕ) : normalize (n : ℤ) = n :=
 normalize_of_nonneg (coe_nat_le_coe_nat_of_le $ nat.zero_le n)
 
-theorem coe_nat_abs_eq_normalize (z : ℤ) : (z.nat_abs : ℤ) = normalize z :=
-begin
-  by_cases 0 ≤ z,
-  { simp [nat_abs_of_nonneg h, normalize_of_nonneg h] },
-  { simp [of_nat_nat_abs_of_nonpos (le_of_not_ge h), normalize_of_neg (lt_of_not_ge h)] }
-end
+lemma abs_eq_normalize (z : ℤ) : |z| = normalize z :=
+by cases le_total 0 z; simp [normalize_of_nonneg, normalize_of_nonpos, *]
 
 lemma nonneg_of_normalize_eq_self {z : ℤ} (hz : normalize z = z) : 0 ≤ z :=
-calc 0 ≤ (z.nat_abs : ℤ) : coe_zero_le _
-... = normalize z : coe_nat_abs_eq_normalize _
-... = z : hz
+abs_eq_self.1 $ by rw [abs_eq_normalize, hz]
 
 lemma nonneg_iff_normalize_eq_self (z : ℤ) : normalize z = z ↔ 0 ≤ z :=
 ⟨nonneg_of_normalize_eq_self, normalize_of_nonneg⟩
@@ -127,7 +125,7 @@ instance : gcd_monoid ℤ :=
   gcd_dvd_right  := assume a b, int.gcd_dvd_right _ _,
   dvd_gcd        := assume a b c, dvd_gcd,
   gcd_mul_lcm    := λ a b, by
-  { rw [← int.coe_nat_mul, gcd_mul_lcm, coe_nat_abs_eq_normalize],
+  { rw [← int.coe_nat_mul, gcd_mul_lcm, coe_nat_abs, abs_eq_normalize],
     exact normalize_associated (a * b) },
   lcm_zero_left  := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_left _,
   lcm_zero_right := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_right _}
@@ -225,10 +223,10 @@ begin
   { refine (assume a, quotient.induction_on' a $ assume a,
       associates.mk_eq_mk_iff_associated.2 $ associated.symm $ ⟨norm_unit a, _⟩),
     show normalize a = int.nat_abs (normalize a),
-    rw [int.coe_nat_abs_eq_normalize, normalize_idem] },
+    rw [int.coe_nat_abs, int.abs_eq_normalize, normalize_idem] },
   { intro n,
     dsimp,
-    rw [←normalize_apply, ← int.coe_nat_abs_eq_normalize, int.nat_abs_of_nat, int.nat_abs_of_nat] }
+    rw [←normalize_apply, ←int.abs_eq_normalize, int.nat_abs_abs, int.nat_abs_of_nat] }
 end
 
 lemma int.prime.dvd_mul {m n : ℤ} {p : ℕ}

src/testing/slim_check/sampleable.lean

@@ -371,7 +371,7 @@ begin
   rcases i with ⟨x,⟨y,hy⟩⟩; unfold_wf;
   dsimp [rat.mk_pnat],
   mono*,
-  { rw [← int.coe_nat_le, ← int.abs_eq_nat_abs, ← int.abs_eq_nat_abs],
+  { rw [← int.coe_nat_le, int.coe_nat_abs, int.coe_nat_abs],
     apply int.abs_div_le_abs },
   { change _ - 1 ≤ y-1,
     apply tsub_le_tsub_right,