Documentation

Mathlib.Tactic.TautoSet

The tauto_set tactic #

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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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