chore: bump Std (#10455)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Tobias Grosser <tobias@grosser.es>

Archive/MiuLanguage/DecisionSuf.lean

@@ -158,7 +158,7 @@ private theorem le_pow2_and_pow2_eq_mod3' (c : ℕ) (x : ℕ) (h : c = 1 ∨ c =
   refine' ⟨g + 2, _, _⟩
   · rw [mul_succ, ← add_assoc, pow_add]
     change c + 3 * k + 3 ≤ 2 ^ g * (1 + 3); rw [mul_add (2 ^ g) 1 3, mul_one]
-    linarith [hkg, one_le_two_pow g]
+    linarith [hkg, @Nat.one_le_two_pow g]
   · rw [pow_add, ← mul_one c]
     exact ModEq.mul hgmod rfl
 

Mathlib/Analysis/PSeries.lean

@@ -78,7 +78,8 @@ theorem sum_condensed_le' (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m
     -- Note(kmill): was `fun k hk => ...` but `mem_Ico.mp hk` was elaborating with some
     -- delayed assignment metavariables that weren't resolved in time. `intro` fixes this.
     intro k hk
-    exact hf (n.one_le_two_pow.trans_lt <| (Nat.lt_succ_of_le le_rfl).trans_le (mem_Ico.mp hk).1)
+    exact hf ((@Nat.one_le_two_pow n).trans_lt <|
+      (Nat.lt_succ_of_le le_rfl).trans_le (mem_Ico.mp hk).1)
       (Nat.le_of_lt_succ <| (mem_Ico.mp hk).2)
   convert sum_le_sum this
   simp [pow_succ, two_mul]

Mathlib/Data/Fin/Basic.lean

@@ -1517,8 +1517,6 @@ protected theorem coe_neg (a : Fin n) : ((-a : Fin n) : ℕ) = (n - a) % n :=
   rfl
 #align fin.coe_neg Fin.coe_neg
 
-protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : ℕ) = (a + (n - b)) % n := by
-  cases a; cases b; rfl
 #align fin.coe_sub Fin.coe_sub
 
 theorem eq_zero (n : Fin 1) : n = 0 := Subsingleton.elim _ _

Mathlib/Data/Nat/Pow.lean

@@ -65,8 +65,6 @@ theorem one_le_pow' (n m : ℕ) : 1 ≤ (m + 1) ^ n :=
   one_le_pow n (m + 1) (succ_pos m)
 #align nat.one_le_pow' Nat.one_le_pow'
 
-theorem one_le_two_pow (n : ℕ) : 1 ≤ 2 ^ n :=
-  one_le_pow n 2 (by decide)
 #align nat.one_le_two_pow Nat.one_le_two_pow
 
 theorem one_lt_pow (n m : ℕ) (h₀ : n ≠ 0) (h₁ : 1 < m) : 1 < m ^ n := by
@@ -85,7 +83,6 @@ theorem one_lt_pow_iff {k n : ℕ} (h : k ≠ 0) : 1 < n ^ k ↔ 1 < n :=
   one_lt_pow_iff_of_nonneg (zero_le _) h
 #align nat.one_lt_pow_iff Nat.one_lt_pow_iff
 
-theorem one_lt_two_pow (n : ℕ) (h₀ : n ≠ 0) : 1 < 2 ^ n := one_lt_pow n 2 h₀ (by decide)
 #align nat.one_lt_two_pow Nat.one_lt_two_pow
 
 theorem one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1) :=

Mathlib/NumberTheory/LucasLehmer.lean

@@ -95,7 +95,7 @@ def sMod (p : ℕ) : ℕ → ℤ
 #align lucas_lehmer.s_mod LucasLehmer.sMod
 
 theorem mersenne_int_pos {p : ℕ} (hp : p ≠ 0) : (0 : ℤ) < 2 ^ p - 1 :=
-  sub_pos.2 <| mod_cast Nat.one_lt_two_pow p hp
+  sub_pos.2 <| mod_cast Nat.one_lt_two_pow hp
 
 theorem mersenne_int_ne_zero (p : ℕ) (hp : p ≠ 0) : (2 ^ p - 1 : ℤ) ≠ 0 :=
   (mersenne_int_pos hp).ne'
@@ -415,7 +415,7 @@ theorem two_lt_q (p' : ℕ) : 2 < q (p' + 2) := by
   refine (minFac_prime (one_lt_mersenne ?_).ne').two_le.lt_of_ne' ?_
   · exact le_add_left _ _
   · rw [Ne.def, minFac_eq_two_iff, mersenne, Nat.pow_succ']
-    exact Nat.two_not_dvd_two_mul_sub_one (Nat.one_le_two_pow _)
+    exact Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow
 #align lucas_lehmer.two_lt_q LucasLehmer.two_lt_q
 
 theorem ω_pow_formula (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) :

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "f1cae6351cf7010d504e6652f05e8aa2da0dd4cb",
+   "rev": "30710c3e6e3c66356b5e37d2c77508eff0fa2357",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",