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.
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
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
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
"Simp attribute for lemmas about RCLike
"
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 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
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
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
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 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
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
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 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)
Instances For
A simp set for the fin_omega
wrapper around omega
.
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
A simp set for simplifying expressions involving ⊤
in enat_to_nat
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A simp set for pushing coercions from ℕ
to ℕ∞
in enat_to_nat
.
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
A simp set for the pnat_to_nat
tactic.
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
mon_tauto
is a simp set to prove tautologies about morphisms from some (tensor) power of M
to M
, where M
is a (commutative) monoid object in a (braided) monoidal category.
This simp
set is incompatible with the standard simp set.
If you want to use it, make sure to add the following to your simp call to disable the problematic
default simp lemmas:
-MonoidalCategory.whiskerLeft_id, -MonoidalCategory.id_whiskerRight,
-MonoidalCategory.tensor_comp, -MonoidalCategory.tensor_comp_assoc,
-MonObj.mul_assoc, -MonObj.mul_assoc_assoc
The general algorithm it follows is to push the associators α_
and commutators β_
inwards until
they cancel against the right sequence of multiplications.
This approach is justified by the fact that a tautology in the language of (commutative) monoid objects "remembers" how it was proved: Every use of a (commutative) monoid object axiom inserts a unitor, associator or commutator, and proving a tautology simply amounts to undoing those moves as prescribed by the presence of unitors, associators and commutators in its expression.
This simp set is opiniated about its normal form, which is why it cannot be used concurrently with some of the simp lemmas in the standard simp set:
- It eliminates all mentions of whiskers by rewriting them to tensored homs,
which goes against
whiskerLeft_id
andid_whiskerRight
:X ◁ f = 𝟙 X ⊗ₘ f
,f ▷ X = 𝟙 X ⊗ₘ f
. This goes againstwhiskerLeft_id
andid_whiskerRight
in the standard simp set. - It collapses compositions of tensored homs to the tensored hom of the compositions,
which goes against
tensor_comp
:(f₁ ⊗ₘ g₁) ≫ (f₂ ⊗ₘ g₂) = (f₁ ≫ f₂) ⊗ₘ (g₁ ≫ g₂)
. TODO: Isn't this direction Just Better? - It cancels the associators against multiplications,
which goes against
mul_assoc
:(α_ M M M).hom ≫ (𝟙 M ⊗ₘ μ) ≫ μ = (μ ⊗ₘ 𝟙 M) ≫ μ
,(α_ M M M).inv ≫ (μ ⊗ₘ 𝟙 M) ≫ μ = (𝟙 M ⊗ₘ μ) ≫ μ
- It unfolds non-primitive coherence isomorphisms, like the tensor strengths
tensorμ
,tensorδ
.
Equations
- One or more equations did not get rendered due to their size.