Documentation

Mathlib.Tactic.Attr.Register

Attributes used in Mathlib #

In this file we define all simp-like and label-like attributes used in Mathlib. We declare all of them in one file for two reasons:

The simpset field_simps is used by the tactic field_simp to reduce an expression in a field to an expression of the form n / d where n and d are division-free.

Instances For

    Simp attribute for lemmas about Even

    Instances For

      "Simp attribute for lemmas about IsROrC"

      Instances For

        The simpset qify_simps is used by the tactic qify to moved expression from or to which gives a well-behaved division.

        Instances For

          The simpset zify_simps is used by the tactic zify to moved expression from to which gives a well-behaved subtraction.

          Instances For

            The simpset mfld_simps records several simp lemmas that are especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it possible to have quicker proofs (when used with squeeze_simp or simp only) while retaining readability.

            The typical use case is the following, in a file on manifolds: If simp [foo, bar] is slow, replace it with squeeze_simp [foo, bar, mfld_simps] and paste its output. The list of lemmas should be reasonable (contrary to the output of squeeze_simp [foo, bar] which might contain tens of lemmas), and the outcome should be quick enough.

            Instances For

              Simp set for integral rules.

              Instances For

                simp set for the manipulation of typevec and arrow expressions

                Instances For

                  Simplification rules for ghost equations.

                  Instances For

                    The @[nontriviality] simp set is used by the nontriviality tactic to automatically discharge theorems about the trivial case (where we know Subsingleton α and many theorems in e.g. groups are trivially true).

                    Instances For

                      A stub attribute for is_poly.

                      Instances For