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:

• in Lean 4, one cannot use an attribute in the same file where it was declared;
• this way it is easy to see which simp sets contain a given lemma.

def Parser.Attr.functor_norm : Lean.ParserDescr

Simp set for functor_norm

def Parser.Attr.monad_norm : Lean.ParserDescr

Simp set for functor_norm

def Parser.Attr.field_simps : Lean.ParserDescr

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.

def Parser.Attr.parity_simps : Lean.ParserDescr

Simp attribute for lemmas about Even

def Parser.Attr.isROrC_simps : Lean.ParserDescr

"Simp attribute for lemmas about IsROrC"

def Parser.Attr.qify_simps : Lean.ParserDescr

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

def Parser.Attr.zify_simps : Lean.ParserDescr

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

def Parser.Attr.mfld_simps : Lean.ParserDescr

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.

def Parser.Attr.integral_simps : Lean.ParserDescr

Simp set for integral rules.

def Parser.Attr.typevec : Lean.ParserDescr

simp set for the manipulation of typevec and arrow expressions

def Parser.Attr.ghost_simps : Lean.ParserDescr

Simplification rules for ghost equations.

def Parser.Attr.nontriviality : Lean.ParserDescr

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).

def Parser.Attr.is_poly : Lean.ParserDescr

A stub attribute for is_poly.