tacticTauto_set — Mathlib

Lean4
/-- `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
```
-/
@[tactic_parser 1000]
public meta def tacticTauto_set : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.TautoSet.tacticTauto_set 1024 (ParserDescr.nonReservedSymbol✝ "tauto_set" false✝)
Похожие утверждения