Merge pull request #531 from Seasawher/auto-update-branch

Lean/Mathlib update

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `04559d2239ba325ddc1fc75fd47f2e321fef41cc`
+Mathlib version: `5b4465844e3feb231af0edb5ef1ab8e2523b08a7`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `04559d2239ba325ddc1fc75fd47f2e321fef41cc`
+Mathlib version: `5b4465844e3feb231af0edb5ef1ab8e2523b08a7`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `04559d2239ba325ddc1fc75fd47f2e321fef41cc`
+Mathlib version: `5b4465844e3feb231af0edb5ef1ab8e2523b08a7`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `04559d2239ba325ddc1fc75fd47f2e321fef41cc`
+Mathlib version: `5b4465844e3feb231af0edb5ef1ab8e2523b08a7`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "04559d2239ba325ddc1fc75fd47f2e321fef41cc",
+   "rev": "5b4465844e3feb231af0edb5ef1ab8e2523b08a7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3",
+   "rev": "0203092c2e5e26edf967000f0e177cf31c72e17a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009064c21bad4d7f421f2901c5e817c8bf3468cb",
+   "rev": "3611075024b3529e5798e53c733671039f06f0bd",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8ef4bdd7a23c3a37170fbd3fa7ee07ef2a54c2d",
+   "rev": "135329b50b116dcc2c021c318c365e82a048856f",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.79",
+   "inputRev": "v0.0.80",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349",
+   "rev": "a2e4d9e9aebdbdce1ce6b6f0a19dd49e0120c990",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2781d8ad404303b2fe03710ac7db946ddfe3539f",
+   "rev": "9bff22d64abde45944c7b1f55bce6c89dd8307e6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5c78955e8375f872c085514cb521216bac1bda17",
+   "rev": "ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "1dae8b12f8ba27576ffe5ddee78bebf6458157b0",
+   "rev": "cd188c6ecfbf6c00cf639e4d4fb18bf773ce8c2c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0",
+   "inputRev": "v4.25.1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«mathlib4-help»",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.0
+leanprover/lean4:v4.25.1