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

Seasawher · Jan 15, 2025 · 5279119 · 5279119
2 parents de120c7 + 1d50ad9
commit 5279119
Show file tree

Hide file tree

Showing 5 changed files with 28 additions and 6 deletions.
diff --git a/docs/attributes.md b/docs/attributes.md
@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `9c0bf76ac298a4b44d6fc4cfc595a4d49f9b0289`
+Mathlib version: `dc5b3f0c90e6e91580442a3ec4df5cf3ee638eb0`
 
 ## aesop
  Register a declaration as an Aesop rule.

diff --git a/docs/commands.md b/docs/commands.md
@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `9c0bf76ac298a4b44d6fc4cfc595a4d49f9b0289`
+Mathlib version: `dc5b3f0c90e6e91580442a3ec4df5cf3ee638eb0`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

diff --git a/docs/options.md b/docs/options.md
@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `9c0bf76ac298a4b44d6fc4cfc595a4d49f9b0289`
+Mathlib version: `dc5b3f0c90e6e91580442a3ec4df5cf3ee638eb0`
 
 ## Elab.async
 type: `Bool`

diff --git a/docs/tactics.md b/docs/tactics.md
@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `9c0bf76ac298a4b44d6fc4cfc595a4d49f9b0289`
+Mathlib version: `dc5b3f0c90e6e91580442a3ec4df5cf3ee638eb0`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -5394,6 +5394,11 @@ from arguments `a₁` ... `aₙ`.
 The tactic adds a new hypothesis with the same name `h := h a₁ ... aₙ`
 and tries to clear the previous one.
 
+## specialize_all
+Defined in: `Mathlib.Tactic.TautoSet.specialize_all`
+
+`specialize_all x` runs `specialize h x` for all hypotheses `h` where this tactic succeeds.
+
 ## split
 Defined in: `Lean.Parser.Tactic.split`
 
@@ -5583,6 +5588,23 @@ The Lean 3 version of this tactic by default attempted to avoid classical reason
 where possible. This Lean 4 version makes no such attempt. The `itauto` tactic
 is designed for that purpose.
 
+## tauto_set
+Defined in: `Mathlib.Tactic.TautoSet.tacticTauto_set`
+
+`tauto_set` attempts to prove tautologies involving hypotheses and goals of the form `X ⊆ Y`
+or `X = Y`, where `X`, `Y` are expressions built using ∪, ∩, \, and ᶜ from finitely many
+variables of type `Set α`. It also unfolds expressions of the form `Disjoint A B` and
+`symmDiff A B`.
+
+Examples:
+```lean
+example {α} (A B C D : Set α) (h1 : A ⊆ B) (h2 : C ⊆ D) : C \ B ⊆ D \ A := by
+  tauto_set
+
+example {α} (A B C : Set α) (h1 : A ⊆ B ∪ C) : (A ∩ B) ∪ (A ∩ C) = A := by
+  tauto_set
+```
+
 ## tfae_finish
 Defined in: `Mathlib.Tactic.TFAE.tfaeFinish`
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9c0bf76ac298a4b44d6fc4cfc595a4d49f9b0289",
+   "rev": "dc5b3f0c90e6e91580442a3ec4df5cf3ee638eb0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
+   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",