The tauto_set tactic

def Mathlib.Tactic.TautoSet.specialize_all : Lean.ParserDescr

specialize_all x runs specialize h x for all hypotheses h where this tactic succeeds.

def Mathlib.Tactic.TautoSet.tacticTauto_set : Lean.ParserDescr

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:

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