chore: adaptations for nightly-2024-04-07 (#12214)

Counterexamples/Phillips.lean

@@ -577,7 +577,7 @@ theorem countable_ne (Hcont : #ℝ = aleph 1) (φ : (DiscreteCopy ℝ →ᵇ ℝ
       ⋃ y ∈ φ.toBoundedAdditiveMeasure.discreteSupport, {x | y ∈ spf Hcont x} := by
     intro x hx
     dsimp at hx
-    rw [← Ne.def, ← nonempty_iff_ne_empty] at hx
+    rw [← Ne, ← nonempty_iff_ne_empty] at hx
     simp only [exists_prop, mem_iUnion, mem_setOf_eq]
     exact hx
   apply Countable.mono (Subset.trans A B)

Mathlib/Data/Nat/Dist.lean

@@ -24,11 +24,11 @@ def dist (n m : ℕ) :=
 -- Should be aligned to `Nat.dist.def`, but that is generated on demand and isn't present yet.
 #noalign nat.dist.def
 
-theorem dist_comm (n m : ℕ) : dist n m = dist m n := by simp [Nat.dist.def, add_comm]
+theorem dist_comm (n m : ℕ) : dist n m = dist m n := by simp [dist, add_comm]
 #align nat.dist_comm Nat.dist_comm
 
 @[simp]
-theorem dist_self (n : ℕ) : dist n n = 0 := by simp [dist.def, tsub_self]
+theorem dist_self (n : ℕ) : dist n n = 0 := by simp [dist, tsub_self]
 #align nat.dist_self Nat.dist_self
 
 theorem eq_of_dist_eq_zero {n m : ℕ} (h : dist n m = 0) : n = m :=
@@ -43,7 +43,7 @@ theorem dist_eq_zero {n m : ℕ} (h : n = m) : dist n m = 0 := by rw [h, dist_se
 #align nat.dist_eq_zero Nat.dist_eq_zero
 
 theorem dist_eq_sub_of_le {n m : ℕ} (h : n ≤ m) : dist n m = m - n := by
-  rw [dist.def, tsub_eq_zero_iff_le.mpr h, zero_add]
+  rw [dist, tsub_eq_zero_iff_le.mpr h, zero_add]
 #align nat.dist_eq_sub_of_le Nat.dist_eq_sub_of_le
 
 theorem dist_eq_sub_of_le_right {n m : ℕ} (h : m ≤ n) : dist n m = n - m :=
@@ -91,13 +91,13 @@ theorem dist_eq_intro {n m k l : ℕ} (h : n + m = k + l) : dist n k = dist l m
 
 theorem dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k := by
   have : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n)) := by
-    simp [dist.def, add_comm, add_left_comm, add_assoc]
-  rw [this, dist.def]
+    simp [dist, add_comm, add_left_comm, add_assoc]
+  rw [this, dist]
   exact add_le_add tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub
 #align nat.dist.triangle_inequality Nat.dist.triangle_inequality
 
 theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k := by
-  rw [dist.def, dist.def, right_distrib, tsub_mul n, tsub_mul m]
+  rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]
 #align nat.dist_mul_right Nat.dist_mul_right
 
 theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m := by
@@ -110,7 +110,7 @@ theorem dist_eq_max_sub_min {i j : ℕ} : dist i j = (max i j) - min i j :=
   (by intro h; rw [max_eq_left h, min_eq_right h, dist_eq_sub_of_le_right h])
 
 theorem dist_succ_succ {i j : Nat} : dist (succ i) (succ j) = dist i j := by
-  simp [dist.def, succ_sub_succ]
+  simp [dist, succ_sub_succ]
 #align nat.dist_succ_succ Nat.dist_succ_succ
 
 theorem dist_pos_of_ne {i j : Nat} : i ≠ j → 0 < dist i j := fun hne =>

Mathlib/NumberTheory/FermatPsp.lean

@@ -365,7 +365,7 @@ theorem exists_infinite_pseudoprimes {b : ℕ} (h : 1 ≤ b) (m : ℕ) :
   · have h₁ : b = 1 := by omega
     rw [h₁]
     use 2 * (m + 2)
-    have : ¬Nat.Prime (2 * (m + 2)) := Nat.not_prime_mul (by norm_num) (by norm_num)
+    have : ¬Nat.Prime (2 * (m + 2)) := Nat.not_prime_mul (by omega) (by omega)
     exact ⟨fermatPsp_base_one (by omega) this, by omega⟩
 #align fermat_psp.exists_infinite_pseudoprimes Nat.exists_infinite_pseudoprimes
 

Mathlib/NumberTheory/ZetaFunction.lean

@@ -753,7 +753,7 @@ theorem riemannZeta_neg_nat_eq_bernoulli (k : ℕ) :
       exact lt_of_le_of_lt
         (by set_option tactic.skipAssignedInstances false in norm_num : (-n : ℤ) ≤ 0)
         (by positivity)
-    · rw [(by norm_cast : 2 * (m : ℂ) + 2 = ↑(2 * m + 2)), Ne, Nat.cast_eq_one]; norm_num
+    · rw [(by norm_cast : 2 * (m : ℂ) + 2 = ↑(2 * m + 2)), Ne, Nat.cast_eq_one]; omega
     -- get rid of sine term
     rw [show Complex.sin (↑π * (1 - (2 * ↑m + 2)) / 2) = -(-1 : ℂ) ^ m by
         rw [(by field_simp; ring : (π : ℂ) * (1 - (2 * ↑m + 2)) / 2 = π / 2 - (π * m + π))]