An identity function with its main argument implicit. This will be printed as hidden even if it is applied to a large term, so it can be used for elision, as done in the elide and unelide tactics.

Ex falso, the nondependent eliminator for the empty type.

Many structures such as bundled morphisms coerce to functions so that you can transparently apply them to arguments. For example, if e : α ≃ β and a : α then you can write e a and this is elaborated as ⇑e a. This type of coercion is implemented using the has_coe_to_fun type class. There is one important consideration:

If a type coerces to another type which in turn coerces to a function, then it must implement has_coe_to_fun directly:

structure sparkling_equiv (α β) extends α ≃ β

-- if we add a `has_coe` instance,
instance {α β} : has_coe (sparkling_equiv α β) (α ≃ β) :=
⟨sparkling_equiv.to_equiv⟩

-- then a `has_coe_to_fun` instance **must** be added as well:
instance {α β} : has_coe_to_fun (sparkling_equiv α β) :=
⟨λ _, α → β, λ f, f.to_equiv.to_fun⟩

(Rationale: if we do not declare the direct coercion, then ⇑e a is not in simp-normal form. The lemma coe_fn_coe_base will unfold it to ⇑↑e a. This often causes loops in the simplifier.)

Ex falso, the nondependent eliminator for the pempty type.

In most cases, we should not have global instances of fact; typeclass search only reads the head symbol and then tries any instances, which means that adding any such instance will cause slowdowns everywhere. We instead make them as lemmata and make them local instances as required.

Swaps two pairs of arguments to a function.

If x : α . tac_name then x.out : α. These are definitionally equal, but this can nevertheless be useful for various reasons, e.g. to apply further projection notation or in an argument to simp.

If x : α := d then x.out : α. These are definitionally equal, but this can nevertheless be useful for various reasons, e.g. to apply further projection notation or in an argument to simp.

Ex falso for negation. From ¬ a and a anything follows. This is the same as absurd with the arguments flipped, but it is in the not namespace so that projection notation can be used.

In most of mathlib, we use the law of excluded middle (LEM) and the axiom of choice (AC) freely. The decidable namespace contains versions of lemmas from the root namespace that explicitly attempt to avoid the axiom of choice, usually by adding decidability assumptions on the inputs.

You can check if a lemma uses the axiom of choice by using #print axioms foo and seeing if classical.choice appears in the list.

As mathlib is primarily classical, if the type signature of a def or lemma does not require any decidable instances to state, it is preferable not to introduce any decidable instances that are needed in the proof as arguments, but rather to use the classical tactic as needed.

In the other direction, when decidable instances do appear in the type signature, it is better to use explicitly introduced ones rather than allowing Lean to automatically infer classical ones, as these may cause instance mismatch errors later.

Transfer decidability of a to decidability of b, if the propositions are equivalent. Important: this function should be used instead of rw on decidable b, because the kernel will get stuck reducing the usage of propext otherwise, and dec_trivial will not work.

Transfer decidability of b to decidability of a, if the propositions are equivalent. This is the same as decidable_of_iff but the iff is flipped.

Prove that a is decidable by constructing a boolean b and a proof that b ↔ a. (This is sometimes taken as an alternate definition of decidability.)