chore: update for leanprover-community/batteries#758 (#12475)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: urkud

Mathlib/Combinatorics/Enumerative/Composition.lean

@@ -714,7 +714,7 @@ theorem get_splitWrtCompositionAux (l : List α) (ns : List ℕ) {i : ℕ} (hi)
   · cases hi
   cases' i with i
   · rw [Nat.add_zero, List.take_zero, sum_nil]
-    simpa using get_zero hi
+    simpa using get_mk_zero hi
   · simp only [splitWrtCompositionAux._eq_2, get_cons_succ, IH, take,
         sum_cons, Nat.add_eq, add_zero, splitAt_eq_take_drop, drop_take, drop_drop]
     rw [Nat.succ_eq_add_one, add_comm (sum _) n, Nat.add_sub_add_left]

Mathlib/Data/List/Basic.lean

@@ -1294,11 +1294,9 @@ theorem nthLe_of_eq {L L' : List α} (h : L = L') {i : ℕ} (hi : i < L.length)
 theorem nthLe_singleton (a : α) {n : ℕ} (hn : n < 1) : nthLe [a] n hn = a := get_singleton ..
 #align list.nth_le_singleton List.nthLe_singleton
 
-@[deprecated] -- 2023-01-05 -- FIXME: replacement -- it's not `get_zero` and it's not `get?_zero`
-theorem nthLe_zero [Inhabited α] {L : List α} (h : 0 < L.length) : List.nthLe L 0 h = L.head! := by
-  cases L
-  cases h
-  simp [nthLe]
+@[deprecated get_mk_zero] -- 2023-01-05
+theorem nthLe_zero {L : List α} (h : 0 < L.length) : List.nthLe L 0 h = L.head (length_pos.1 h) :=
+  get_mk_zero h
 #align list.nth_le_zero List.nthLe_zero
 
 #align list.nth_le_append List.get_append

Mathlib/Data/List/Rotate.lean

@@ -592,14 +592,14 @@ theorem get_cyclicPermutations (l : List α) (n : Fin (length (cyclicPermutation
 #align list.nth_le_cyclic_permutations List.get_cyclicPermutations
 
 @[simp]
-theorem head?_cyclicPermutations (l : List α) : (cyclicPermutations l).head? = l := by
+theorem head_cyclicPermutations (l : List α) :
+    (cyclicPermutations l).head (cyclicPermutations_ne_nil l) = l := by
   have h : 0 < length (cyclicPermutations l) := length_pos_of_ne_nil (cyclicPermutations_ne_nil _)
-  simp_rw [← get_zero h, get_cyclicPermutations, rotate_zero]
+  rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]
 
 @[simp]
-theorem head_cyclicPermutations (l : List α) :
-    (cyclicPermutations l).head (cyclicPermutations_ne_nil l) = l := by
-  rw [← Option.some_inj, ← head?_eq_head, head?_cyclicPermutations]
+theorem head?_cyclicPermutations (l : List α) : (cyclicPermutations l).head? = l := by
+  rw [head?_eq_head, head_cyclicPermutations]
 
 theorem cyclicPermutations_injective : Function.Injective (@cyclicPermutations α) := fun l l' h ↦ by
   simpa using congr_arg head? h

Mathlib/NumberTheory/Zsqrtd/Basic.lean

@@ -899,7 +899,7 @@ theorem divides_sq_eq_zero {x y} (h : x * x = d * y * y) : x = 0 ∧ y = 0 :=
   Or.elim g.eq_zero_or_pos
     (fun H => ⟨Nat.eq_zero_of_gcd_eq_zero_left H, Nat.eq_zero_of_gcd_eq_zero_right H⟩) fun gpos =>
     False.elim <| by
-      let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime gpos
+      let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime _ _
       rw [hx, hy] at h
       have : m * m = d * (n * n) := by
         refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_

lake-manifest.json

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