chore: review adaptions for leanprover/lean4#6200

leanprover-community · Nov 26, 2024 · c94e3c9 · c94e3c9
1 parent 5e5178b
commit c94e3c9
Show file tree

Hide file tree

Showing 7 changed files with 7 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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}