chore: bump to v4.17.0-rc1

FLT/MathlibExperiments/HopfAlgebra/Basic.lean

@@ -73,7 +73,6 @@ lemma antipode_unique {T : LinearPoint R A A} (h : T * LinearMap.id = 1) :
     T = antipode :=
   left_inv_eq_right_inv (M := LinearPoint R A A) h id_mul_antipode
 
-
 lemma antipode_unique' {T : LinearPoint R A A} (h : LinearMap.id * T = 1) :
     T = antipode :=
   left_inv_eq_right_inv (M := LinearPoint R A A) antipode_mul_id h |>.symm

docbuild/lakefile.toml

@@ -10,4 +10,4 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.16.0"
+rev = "main"

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02",
+   "rev": "8618f3e87c85cd2868f17762ac7fa7fa9c79fd3a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "stable",
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
+   "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e",
+   "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,37 +55,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
+   "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.50",
+   "inputRev": "v0.0.52-pre",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
+   "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "rev": "7b3b0c8327b3c0214ac49ca6d6922edbb81ab8c9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e",
+   "rev": "3766e2340b4f89b1173910f0161ca8eded9b0902",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -8,7 +8,7 @@ package FLT where
     ⟨`relaxedAutoImplicit, false⟩ -- switch off relaxed auto-implicit
   ]
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "stable"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "master"
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.16.0
+leanprover/lean4:v4.17.0-rc1