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