# 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` 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

Equations

- Mathlib.Tactic.TautoSet.tacticTauto_set = Lean.ParserDescr.node `Mathlib.Tactic.TautoSet.tacticTauto_set 1024 (Lean.ParserDescr.nonReservedSymbol "tauto_set" false)

Instances For