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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `b6513d2f3e7b05fa944382687824be4b8b4bb5ef`
+Mathlib version: `4d3317200498df0e4852e99d09728b257857d066`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `b6513d2f3e7b05fa944382687824be4b8b4bb5ef`
+Mathlib version: `4d3317200498df0e4852e99d09728b257857d066`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`
@@ -2008,23 +2008,11 @@ Defined in: `Batteries.Util.LibraryNote.commandLibrary_note____1`
 
 Support the old `library_note "foo"` syntax, with a deprecation warning.
 
-## library_note2
-Defined in: `commandLibrary_note2____1`
-
-Support the old `library_note "foo"` syntax, with a deprecation warning.
-
 ## library_note2
 Defined in: `Batteries.Util.LibraryNote.commandLibrary_note2___`
 
 Support the old `library_note2 «foo»` syntax, with a deprecation warning.
 
-## library_note2
-Defined in: `commandLibrary_note2___`
-
-`library_note2 «my note» /-- documentation -/` creates a library note named `my note`
-in the `Mathlib.LibraryNote` namespace, whose content is `/-- documentation -/`.
-You can access this note using, for example, `#print Mathlib.LibraryNote.«my note»`.
-
 ## library_note2
 Defined in: `Batteries.Util.LibraryNote.commandLibrary_note2____1`
 

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `b6513d2f3e7b05fa944382687824be4b8b4bb5ef`
+Mathlib version: `4d3317200498df0e4852e99d09728b257857d066`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `b6513d2f3e7b05fa944382687824be4b8b4bb5ef`
+Mathlib version: `4d3317200498df0e4852e99d09728b257857d066`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -2272,7 +2272,7 @@ useless for proving theorems. To actually insert an `ite` application use
 Defined in: `Mathlib.Tactic.ENatToNat.tacticEnat_to_nat`
 
 `enat_to_nat` shifts all `ENat`s in the context to `Nat`, rewriting propositions about them.
-A typical use case is `enat_to_nat; omega`.
+A typical use case is `enat_to_nat; lia`.
 
 ## eq_refl
 Defined in: `Lean.Parser.Tactic.eqRefl`
@@ -5935,7 +5935,7 @@ For each `x : PNat` in the context, add the hypothesis `0 < (↑x : ℕ)`.
 Defined in: `Mathlib.Tactic.PNatToNat.tacticPnat_to_nat`
 
 `pnat_to_nat` shifts all `PNat`s in the context to `Nat`, rewriting propositions about them.
-A typical use case is `pnat_to_nat; omega`.
+A typical use case is `pnat_to_nat; lia`.
 
 ## polyrith
 Defined in: `Mathlib.Tactic.Polyrith.«tacticPolyrithOnly[_]»`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b6513d2f3e7b05fa944382687824be4b8b4bb5ef",
+   "rev": "4d3317200498df0e4852e99d09728b257857d066",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",