chore: bump dependencies (#10625)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Feb 18, 2024 · 746ffd5 · 746ffd5
1 parent dcfd3b1
commit 746ffd5
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
@@ -261,7 +261,6 @@ theorem divInt_one (n : ℤ) : n /. 1 = n :=
   show divInt _ _ = _ by
     rw [divInt]
     simp [mkRat, normalize]
-    rfl
 
 theorem mkRat_one {n : ℤ} : mkRat n 1 = n := by
   simp [Rat.mkRat_eq, Rat.divInt_one]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "1b4e6926f03a1f76c16b00c7b6d4891788738a24",
+   "rev": "4c366aba55d28778421b8a1841e5512fd5c53c43",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",