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

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `419be563ec4b4d865cb59bacd8648f872b1a27de`
+Mathlib version: `f0de78130c864056baeec6eff00c438699aec635`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `419be563ec4b4d865cb59bacd8648f872b1a27de`
+Mathlib version: `f0de78130c864056baeec6eff00c438699aec635`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `419be563ec4b4d865cb59bacd8648f872b1a27de`
+Mathlib version: `f0de78130c864056baeec6eff00c438699aec635`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `419be563ec4b4d865cb59bacd8648f872b1a27de`
+Mathlib version: `f0de78130c864056baeec6eff00c438699aec635`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -7886,6 +7886,14 @@ In this way, the wlog-claim `this` can be applied to `x` and `y` in different or
 
 By default, the entire context is reverted.
 
+## wlog!
+Defined in: `Mathlib.Tactic.wlog!`
+
+`wlog! h : P` is a variant of the `wlog h : P` tactic that also calls `push_neg` at the generated
+hypothesis `h : ¬ p` in the side goal. `wlog! h : P ∧ Q` will transform `¬ (P ∧ Q)` to `P → ¬ Q`,
+while  `wlog! +distrib h : P ∧ Q` will transform `¬ (P ∧ Q)` to `P ∨ Q`. For more information, see
+the documentation on `push_neg`.
+
 ## zify
 Defined in: `Mathlib.Tactic.Zify.zify`
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "419be563ec4b4d865cb59bacd8648f872b1a27de",
+   "rev": "f0de78130c864056baeec6eff00c438699aec635",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",