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

Lean/Mathlib update

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `33b1098d29f8e518cf75f3787f93809926385252`
+Mathlib version: `912a3b5ba3932336601feaa9f4a2a80fbe5a0d67`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `33b1098d29f8e518cf75f3787f93809926385252`
+Mathlib version: `912a3b5ba3932336601feaa9f4a2a80fbe5a0d67`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `33b1098d29f8e518cf75f3787f93809926385252`
+Mathlib version: `912a3b5ba3932336601feaa9f4a2a80fbe5a0d67`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `33b1098d29f8e518cf75f3787f93809926385252`
+Mathlib version: `912a3b5ba3932336601feaa9f4a2a80fbe5a0d67`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -1036,6 +1036,16 @@ Defined in: `«tacticBy_cases_:_»`
 
 `by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
 
+## by_cases!
+Defined in: `byCases!`
+
+`by_cases! h : p` runs the `by_cases h : p` tactic, followed by
+`try push_neg at h` in the second subgoal. For example,
+- `by_cases! h : a < b` creates one goal with hypothesis `h : a < b` and
+  another with `h : b ≤ a`.
+- `by_cases! h : a ≠ b` creates one goal with hypothesis `h : a ≠ b` and
+  another with `h : a = b`.
+
 ## by_contra
 Defined in: `Batteries.Tactic.byContra`
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "33b1098d29f8e518cf75f3787f93809926385252",
+   "rev": "912a3b5ba3932336601feaa9f4a2a80fbe5a0d67",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c029ceb9956ef9d567fc034e5403ec829f8d0d87",
+   "rev": "5da171049c81931a2110303c9d547f5ab2955b06",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",