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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `18978c91c03a85d86b990dffa6d69336c85dfb2f`
+Mathlib version: `98379c78c5dd2e3614cd24ab7ad22f5713e0eb63`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `18978c91c03a85d86b990dffa6d69336c85dfb2f`
+Mathlib version: `98379c78c5dd2e3614cd24ab7ad22f5713e0eb63`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `18978c91c03a85d86b990dffa6d69336c85dfb2f`
+Mathlib version: `98379c78c5dd2e3614cd24ab7ad22f5713e0eb63`
 
 ## Elab.async
 type: `Bool`
@@ -979,14 +979,7 @@ type: `Bool`
 
 default: `false`
 
-enable the commandStart linter
-
-## linter.style.commandStart.verbose
-type: `Bool`
-
-default: `false`
-
-enable the commandStart linter
+deprecated: use the `linter.style.whitespace` option instead
 
 ## linter.style.docString
 type: `Bool`
@@ -1121,6 +1114,20 @@ default: `false`
 
 enable the show linter
 
+## linter.style.whitespace
+type: `Bool`
+
+default: `false`
+
+enable the whitespace linter
+
+## linter.style.whitespace.verbose
+type: `Bool`
+
+default: `false`
+
+report diagnostic information for the `whitespace` linter
+
 ## linter.suspiciousUnexpanderPatterns
 type: `Bool`
 

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `18978c91c03a85d86b990dffa6d69336c85dfb2f`
+Mathlib version: `98379c78c5dd2e3614cd24ab7ad22f5713e0eb63`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -4534,10 +4534,9 @@ for the tactic call in case of success.
 ## mem_tac
 Defined in: `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.tacticMem_tac`
 
-
-## mem_tac_aux
-Defined in: `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.tacticMem_tac_aux`
-
+`mem_tac` tries to prove goals of the form `x ∈ 𝒜 i` when `x` has the form of:
+* `y ^ n` where `i = n • j` and `y ∈ 𝒜 j`.
+* a natural number `n`.
 
 ## mexact
 Defined in: `Lean.Parser.Tactic.mexactMacro`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "18978c91c03a85d86b990dffa6d69336c85dfb2f",
+   "rev": "98379c78c5dd2e3614cd24ab7ad22f5713e0eb63",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ee6aea0e5df556046044fe713dfbdc95196d9c9e",
+   "rev": "4eff6c5186ebd4dd594eda5b169aef9a55a8b6d2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",