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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `8ee8525c1e1c3a2794c2bfa32465f220ecf0d1a4`
+Mathlib version: `07f1b273c8871bec3f61440bb61babe43ae4d932`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas
@@ -124,6 +124,30 @@ Finally, if no argument is provided to the `algebraize` attribute, it is assumed
 declaration has name `RingHom.Property` and that the corresponding `Algebra` property has name
 `Algebra.Property`. The attribute then returns `Algebra.Property` (so assume case 1 above).
 
+## aliasIn
+ create alias in another namespace
+Adds an alias of this declaration in a different namespace.
+Example:
+```lean
+@[alias_in Foo.Bar] def A.B.C.d := ...
+```
+behaves like
+```
+alias A.Foo.Bar.d := A.B.C.d
+```
+You can see the name of the alias by mousing over the name argument of `alias_in`.
+
+We replace the rightmost/innermost namespaces, but always leave the final part of the name intact.
+By default, `alias_in` assumes that we want to replace the same number of namespaces from the
+original name as given in the new namespace. You can override this by adding a number at the end
+```
+@[alias_in Foo.Bar 3] def A.B.C.d := ...
+```
+behaves like
+```
+alias Foo.Bar.d := A.B.C.d
+```
+
 ## always_inline
  mark definition to be always inlined
 Changes the inlining behavior. This attribute comes in several variants:

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `8ee8525c1e1c3a2794c2bfa32465f220ecf0d1a4`
+Mathlib version: `07f1b273c8871bec3f61440bb61babe43ae4d932`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `8ee8525c1e1c3a2794c2bfa32465f220ecf0d1a4`
+Mathlib version: `07f1b273c8871bec3f61440bb61babe43ae4d932`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `8ee8525c1e1c3a2794c2bfa32465f220ecf0d1a4`
+Mathlib version: `07f1b273c8871bec3f61440bb61babe43ae4d932`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -2664,11 +2664,11 @@ Defined in: `Lean.Parser.Tactic.focus`
 Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred.
 
 ## forward
-Defined in: `Aesop.Frontend.tacticForward___`
+Defined in: `Aesop.Frontend.tacticForward____`
 
 
 ## forward?
-Defined in: `Aesop.Frontend.tacticForward?___`
+Defined in: `Aesop.Frontend.tacticForward?____`
 
 
 ## frac_tac
@@ -6956,11 +6956,11 @@ Defined in: `Lean.Parser.Tactic.tacticRwa__`
 `rwa` is short-hand for `rw; assumption`.
 
 ## saturate
-Defined in: `Aesop.Frontend.tacticSaturate_____`
+Defined in: `Aesop.Frontend.saturate`
 
 
 ## saturate?
-Defined in: `Aesop.Frontend.tacticSaturate?_____`
+Defined in: `Aesop.Frontend.saturate?`
 
 
 ## says

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8ee8525c1e1c3a2794c2bfa32465f220ecf0d1a4",
+   "rev": "07f1b273c8871bec3f61440bb61babe43ae4d932",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
+   "rev": "e2a2ee109182182dd0e347e8149d312d72bfbfb2",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
+   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
+   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
+   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
+   "rev": "78129e1913fe4988ac238156ec5f223ec02d286c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",