chore: update dependencies (#12792)

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: 3 people

Mathlib/Data/List/OfFn.lean

@@ -36,23 +36,28 @@ namespace List
 
 #noalign list.length_of_fn_aux
 
+@[simp]
+theorem length_ofFn_go {n} (f : Fin n → α) (i j h) : length (ofFn.go f i j h) = i := by
+  induction i generalizing j <;> simp_all [ofFn.go]
+
 /-- The length of a list converted from a function is the size of the domain. -/
 @[simp]
 theorem length_ofFn {n} (f : Fin n → α) : length (ofFn f) = n := by
-  simp [ofFn]
+  simp [ofFn, length_ofFn_go]
 #align list.length_of_fn List.length_ofFn
 
 #noalign list.nth_of_fn_aux
 
+theorem get_ofFn_go {n} (f : Fin n → α) (i j h) (k) (hk) :
+    get (ofFn.go f i j h) ⟨k, hk⟩ = f ⟨j + k, by simp at hk; omega⟩ := by
+  let i+1 := i
+  cases k <;> simp [ofFn.go, get_ofFn_go (i := i)]
+  congr 2; omega
+
 -- Porting note (#10756): new theorem
 @[simp]
 theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f (Fin.cast (by simp) i) := by
-  have := Array.getElem_ofFn f i (by simpa using i.2)
-  cases' i with i hi
-  simp only [getElem, Array.get] at this
-  simp only [Fin.cast_mk]
-  rw [← this]
-  congr
+  cases i; simp [ofFn, get_ofFn_go]
 
 /-- The `n`th element of a list -/
 @[simp]
@@ -114,7 +119,7 @@ theorem ofFn_zero (f : Fin 0 → α) : ofFn f = [] :=
 theorem ofFn_succ {n} (f : Fin (succ n) → α) : ofFn f = f 0 :: ofFn fun i => f i.succ :=
   ext_get (by simp) (fun i hi₁ hi₂ => by
     cases i
-    · simp
+    · simp; rfl
     · simp)
 #align list.of_fn_succ List.ofFn_succ
 

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

@@ -334,8 +334,8 @@ theorem ιMulti_zero_apply (v : Fin 0 → M) : ιMulti R 0 v = 1 :=
 
 @[simp]
 theorem ιMulti_succ_apply {n : ℕ} (v : Fin n.succ → M) :
-    ιMulti R _ v = ι R (v 0) * ιMulti R _ (Matrix.vecTail v) :=
-  (congr_arg List.prod (List.ofFn_succ _)).trans List.prod_cons
+    ιMulti R _ v = ι R (v 0) * ιMulti R _ (Matrix.vecTail v) := by
+  simp [ιMulti, Matrix.vecTail]
 #align exterior_algebra.ι_multi_succ_apply ExteriorAlgebra.ιMulti_succ_apply
 
 theorem ιMulti_succ_curryLeft {n : ℕ} (m : M) :

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "rev": "cac5bff36ff3c339d8fdb0d1506ec789ce57a6fd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
+   "rev": "093226b2a8c0cdeac12f1b4786827c67c673b4fb",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
+   "rev": "e9fb4ecc5d718eb36faae5308880cd3f243788df",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",