From c94e3c95ae70b241286428eccbef27576aef040e Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 26 Nov 2024 01:20:31 -0500 Subject: [PATCH] chore: review adaptions for leanprover/lean4#6200 --- Mathlib/Computability/Ackermann.lean | 2 +- Mathlib/Data/ENNReal/Inv.lean | 2 +- Mathlib/Data/Nat/BitIndices.lean | 2 +- Mathlib/Data/Nat/Factorization/Basic.lean | 2 +- Mathlib/Dynamics/Newton.lean | 2 +- Mathlib/NumberTheory/FactorisationProperties.lean | 2 +- Mathlib/Topology/Algebra/PontryaginDual.lean | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/Computability/Ackermann.lean b/Mathlib/Computability/Ackermann.lean index 84d4c197c5587..92b4e6f1c3a1a 100644 --- a/Mathlib/Computability/Ackermann.lean +++ b/Mathlib/Computability/Ackermann.lean @@ -235,7 +235,7 @@ private theorem sq_le_two_pow_add_one_minus_three (n : ℕ) : n ^ 2 ≤ 2 ^ (n + norm_num apply succ_le_of_lt rw [Nat.pow_succ, mul_comm _ 2, mul_lt_mul_left (zero_lt_two' ℕ)] - exact Nat.lt_two_pow + exact Nat.lt_two_pow_self · rw [Nat.pow_succ, Nat.pow_succ] linarith [one_le_pow k 2 zero_lt_two] diff --git a/Mathlib/Data/ENNReal/Inv.lean b/Mathlib/Data/ENNReal/Inv.lean index 36003f724d580..ce120819caeaa 100644 --- a/Mathlib/Data/ENNReal/Inv.lean +++ b/Mathlib/Data/ENNReal/Inv.lean @@ -533,7 +533,7 @@ theorem exists_inv_two_pow_lt (ha : a ≠ 0) : ∃ n : ℕ, 2⁻¹ ^ n < a := by refine ⟨n, lt_trans ?_ hn⟩ rw [← ENNReal.inv_pow, ENNReal.inv_lt_inv] norm_cast - exact n.lt_two_pow + exact n.lt_two_pow_self @[simp, norm_cast] theorem coe_zpow (hr : r ≠ 0) (n : ℤ) : (↑(r ^ n) : ℝ≥0∞) = (r : ℝ≥0∞) ^ n := by diff --git a/Mathlib/Data/Nat/BitIndices.lean b/Mathlib/Data/Nat/BitIndices.lean index 659563741e3e6..8c4e3d74b89f5 100644 --- a/Mathlib/Data/Nat/BitIndices.lean +++ b/Mathlib/Data/Nat/BitIndices.lean @@ -114,6 +114,6 @@ theorem two_pow_le_of_mem_bitIndices (ha : a ∈ n.bitIndices) : 2^a ≤ n := by exact List.single_le_sum (by simp) _ <| mem_map_of_mem _ ha theorem not_mem_bitIndices_self (n : ℕ) : n ∉ n.bitIndices := - fun h ↦ (n.lt_two_pow).not_le <| two_pow_le_of_mem_bitIndices h + fun h ↦ (n.lt_two_pow_self).not_le <| two_pow_le_of_mem_bitIndices h end Nat diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 73b4652c0c4a3..15659840ed9b9 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -356,7 +356,7 @@ theorem dvd_iff_prime_pow_dvd_dvd (n d : ℕ) : · simp rcases eq_or_ne d 0 with (rfl | hd) · simp only [zero_dvd_iff, hn, false_iff, not_forall] - exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow).not_le⟩ + exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow_self).not_le⟩ refine ⟨fun h p k _ hpkd => dvd_trans hpkd h, ?_⟩ rw [← factorization_prime_le_iff_dvd hd hn] intro h p pp diff --git a/Mathlib/Dynamics/Newton.lean b/Mathlib/Dynamics/Newton.lean index 3d992313b0958..3a68a8bf036e7 100644 --- a/Mathlib/Dynamics/Newton.lean +++ b/Mathlib/Dynamics/Newton.lean @@ -111,7 +111,7 @@ theorem exists_unique_nilpotent_sub_and_aeval_eq_zero · -- Existence obtain ⟨n, hn⟩ := id h refine ⟨P.newtonMap^[n] x, isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n, ?_⟩ - rw [← zero_dvd_iff, ← pow_eq_zero_of_le (n.lt_two_pow).le hn] + rw [← zero_dvd_iff, ← pow_eq_zero_of_le (n.lt_two_pow_self).le hn] exact aeval_pow_two_pow_dvd_aeval_iterate_newtonMap h h' n · -- Uniqueness have ⟨u, hu⟩ := binomExpansion (P.map (algebraMap R S)) r₁ (r₂ - r₁) diff --git a/Mathlib/NumberTheory/FactorisationProperties.lean b/Mathlib/NumberTheory/FactorisationProperties.lean index 206eadd98f223..f32fbb70c0910 100644 --- a/Mathlib/NumberTheory/FactorisationProperties.lean +++ b/Mathlib/NumberTheory/FactorisationProperties.lean @@ -185,7 +185,7 @@ theorem infinite_even_deficient : {n : ℕ | Even n ∧ n.Deficient}.Infinite := constructor · exact ⟨⟨2 ^ n, by ring⟩, prime_two.deficient_pow⟩ · calc - n ≤ 2 ^ n := Nat.le_of_lt n.lt_two_pow + n ≤ 2 ^ n := Nat.le_of_lt n.lt_two_pow_self _ < 2 ^ (n + 1) := (Nat.pow_lt_pow_iff_right (Nat.one_lt_two)).mpr (lt_add_one n) theorem infinite_odd_deficient : {n : ℕ | Odd n ∧ n.Deficient}.Infinite := by diff --git a/Mathlib/Topology/Algebra/PontryaginDual.lean b/Mathlib/Topology/Algebra/PontryaginDual.lean index d2fe0b2b85cf9..2b24a7b06909d 100644 --- a/Mathlib/Topology/Algebra/PontryaginDual.lean +++ b/Mathlib/Topology/Algebra/PontryaginDual.lean @@ -73,7 +73,7 @@ instance [LocallyCompactSpace H] : LocallyCompactSpace (PontryaginDual H) := by refine lt_of_lt_of_le ht ?_ rw [div_le_iff₀' (pow_pos two_pos _), ← div_le_iff₀ hx] refine (Nat.le_ceil (Real.pi / x)).trans ?_ - exact_mod_cast (Nat.le_succ _).trans Nat.lt_two_pow.le + exact_mod_cast (Nat.le_succ _).trans Nat.lt_two_pow_self.le variable {A B C G}