From b002a72900574ecaf6dabaa1e05a4208175e5a56 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 17 Apr 2024 13:17:44 +0000 Subject: [PATCH] chore: adaptations for nightly-2024-04-07 (#12214) --- Counterexamples/Phillips.lean | 2 +- Mathlib/Data/Nat/Dist.lean | 14 +++++++------- Mathlib/NumberTheory/FermatPsp.lean | 2 +- Mathlib/NumberTheory/ZetaFunction.lean | 2 +- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean index 5f96d29afc512..215fac26c6460 100644 --- a/Counterexamples/Phillips.lean +++ b/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) diff --git a/Mathlib/Data/Nat/Dist.lean b/Mathlib/Data/Nat/Dist.lean index e27026a220fb4..abc714c00df14 100644 --- a/Mathlib/Data/Nat/Dist.lean +++ 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 => diff --git a/Mathlib/NumberTheory/FermatPsp.lean b/Mathlib/NumberTheory/FermatPsp.lean index 8df20c14b1710..798bb10c0400c 100644 --- a/Mathlib/NumberTheory/FermatPsp.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ZetaFunction.lean b/Mathlib/NumberTheory/ZetaFunction.lean index bb7fa4b2fb7ca..6926faed68452 100644 --- a/Mathlib/NumberTheory/ZetaFunction.lean +++ b/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 + π))]