update mathlib

MathPuzzles/Imo1989Q5.lean

@@ -211,7 +211,7 @@ problem imo1989_q5 (n : ℕ) : ∃ m, ∀ j < n, ¬IsPrimePow (m + j) := by
   have h1 := hm (ci.get ⟨j, hj1⟩) (List.get_mem _ _ _)
   obtain ⟨h2, h3⟩ := hl (l.get ⟨j, hj2⟩) (List.get_mem _ _ _)
   obtain ⟨h4, _⟩ := hl (l.get ⟨j + n, hj3⟩) (List.get_mem _ _ _)
-  simp only [List.get_ofFn, ge_iff_le, Fin.castIso_mk] at h1
+  simp only [List.get_ofFn, ge_iff_le, Fin.cast_mk] at h1
   have h6 := Nat.ModEq.add_right j h1
   have h7 : j ≤ l.get ⟨j, hj2⟩ * l.get ⟨j + n, hj3⟩ := by
       apply Nat.le_of_lt

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "6f8e81040eae7655f51d145b8026569b91d66e0d",
+    "rev": "bfaffcf10e6d088ae7c1c22462cbd7ae46f6c358",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "6f8e81040eae7655f51d145b8026569b91d66e0d",
+    "inputRev?": "bfaffcf10e6d088ae7c1c22462cbd7ae46f6c358",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",

lakefile.lean

@@ -12,4 +12,4 @@ lean_exe buildWebpage where
   root := `scripts.buildWebpage
   supportInterpreter := true
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "6f8e81040eae7655f51d145b8026569b91d66e0d"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "bfaffcf10e6d088ae7c1c22462cbd7ae46f6c358"