Documentation

Mathlib.Tactic.TautoSet

The tauto_set tactic #

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

tauto_set proves 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. In other words, this tactic proves propositional tautologies, expressed in the language of sets. This is a finishing tactic: it either closes the goal or raises an error.

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
Equations
Instances For