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

Simp set for `functor_norm`

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simp set for `functor_norm`

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simp attribute for lemmas about `Even`

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

"Simp attribute for lemmas about `RCLike`

"

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The simpset `rify_simps`

is used by the tactic `rify`

to move expressions from `ℕ`

, `ℤ`

, or
`ℚ`

to `ℝ`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The simpset `qify_simps`

is used by the tactic `qify`

to move expressions from `ℕ`

or `ℤ`

to `ℚ`

which gives a well-behaved division.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The simpset `zify_simps`

is used by the tactic `zify`

to move expressions from `ℕ`

to `ℤ`

which gives a well-behaved subtraction.

## Equations

- One or more equations did not get rendered due to their size.

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simp set for integral rules.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

simp set for the manipulation of typevec and arrow expressions

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification rules for ghost equations.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Simplification procedure

## Equations

- One or more equations did not get rendered due to their size.

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

A stub attribute for `is_poly`

.

## Equations

- Parser.Attr.is_poly = Lean.ParserDescr.node `Parser.Attr.is_poly 1024 (Lean.ParserDescr.nonReservedSymbol "is_poly" false)