update mathlib

Compfiles/Imo1968P2.lean

@@ -22,14 +22,6 @@ namespace Imo1968P2
 
 snip begin
 
-@[simp] theorem List.enum_eq_nil {α : Type*} {l : List α}
-    : List.enum l = [] ↔ l = [] := by
-  cases l <;> simp [List.enum_cons]
-
-@[simp] theorem List.mapIdx_eq_nil {α β : Type*} {f : ℕ → α → β} {l : List α}
-    : List.mapIdx f l = [] ↔ l = [] := by
-  rw [List.mapIdx_eq_enum_map, List.map_eq_nil, List.enum_eq_nil]
-
 lemma lemma0 {α β : Type} {f : ℕ → α → β} (l : List α) (h2 : l ≠ []) :
     List.getLast (List.mapIdx f l) (List.mapIdx_eq_nil.not.mpr h2) =
     f (l.dropLast).length (List.getLast l h2) := by

lake-manifest.json

@@ -49,10 +49,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "555fddebd3b21542478319c662bc1be696f9178c",
+   "rev": "0cacf073edcc85fd82975c59ea3dbb4bb15a45db",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "555fddebd3b21542478319c662bc1be696f9178c",
+   "inputRev": "0cacf073edcc85fd82975c59ea3dbb4bb15a45db",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "compfiles",

lakefile.lean

@@ -25,4 +25,4 @@ lean_exe checkSolution where
   root := `scripts.checkSolution
   supportInterpreter := true
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "555fddebd3b21542478319c662bc1be696f9178c"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "0cacf073edcc85fd82975c59ea3dbb4bb15a45db"