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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `6e5c57744c0c760f11f5a74683da6c6ff1e73816`
+Mathlib version: `395140bc16632d76426ee2da966b4add3c9a6215`
 
 ## aesop
  Register a declaration as an Aesop rule.

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `6e5c57744c0c760f11f5a74683da6c6ff1e73816`
+Mathlib version: `395140bc16632d76426ee2da966b4add3c9a6215`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `6e5c57744c0c760f11f5a74683da6c6ff1e73816`
+Mathlib version: `395140bc16632d76426ee2da966b4add3c9a6215`
 
 ## Mathlib.Tactic.TFAE.useDeprecated
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `6e5c57744c0c760f11f5a74683da6c6ff1e73816`
+Mathlib version: `395140bc16632d76426ee2da966b4add3c9a6215`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -5733,6 +5733,18 @@ To use `unfold?`, shift-click an expression in the tactic state.
 This gives a list of rewrite suggestions for the selected expression.
 Click on a suggestion to replace `unfold?` by a tactic that performs this rewrite.
 
+## unfold_let
+Defined in: `Mathlib.Tactic.unfoldLetStx`
+
+This tactic is subsumed by the `unfold` tactic.
+
+`unfold_let x y z at loc` unfolds the local definitions `x`, `y`, and `z` at the given
+location, which is known as "zeta reduction."
+This also exists as a `conv`-mode tactic.
+
+If no local definitions are given, then all local definitions are unfolded.
+This variant also exists as the `conv`-mode tactic `zeta`.
+
 ## unfold_projs
 Defined in: `Mathlib.Tactic.unfoldProjsStx`
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "44f2360f50d0d3aea24653103a3f11ef5de9eb90",
+   "rev": "e0d84490d3dc76e242e49bf303d22411ff449e16",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
+   "rev": "39119d25ce6f40a6250b742c6b4e8d9b400af677",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e5c57744c0c760f11f5a74683da6c6ff1e73816",
+   "rev": "395140bc16632d76426ee2da966b4add3c9a6215",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",