Find a lemma¶

Mathlib has hundreds of thousands of lemmas, and most proofs need a few of them. This page shows how to find the one that closes a goal, from the quickest method to the most thorough.

Guess the name¶

Mathlib names follow a convention that makes names guessable. A lemma is named after its conclusion, followed by of and its hypotheses. A weak inequality from a strict one is therefore le_of_lt, and #check confirms the guess and shows the exact statement:

le_of_lt.{u_1} {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) : a ≤ b

The common abbreviations are lt and le for < and ≤, eq and ne for = and ≠, add, mul and sub for the operations, and comm and assoc for commutativity and associativity. So lt_of_le_of_ne turns a ≤ b and a ≠ b into a < b, and add_comm says a + b = b + a.

Search tactics¶

When the name will not come, put a search tactic where the proof should go. exact? looks for a single lemma that closes the goal using the hypotheses in the context. On the goal a ≤ b with a hypothesis smaller : a < b it answers:

Try this:
  [apply] exact Std.le_of_lt smaller

The suggestion replaces exact? in the file when clicked in VS Code's infoview, or accepted with \s in Neovim. apply? also accepts lemmas that leave further goals, and rw? looks for an equation to rewrite with:

Try this:
  [apply] rw [AddSemigroup.add_assoc]
  -- no goals

The search runs over whatever the file imports, so a lemma from an unimported part of Mathlib will not be found. It works offline.

Web search¶

Two commands search Mathlib through web services, and so need an internet connection. #loogle searches by the shape of a statement, and #leansearch by a description in words. Both are available once a file has import Mathlib.Tactic.Common, or all of Mathlib. The Loogle website offers the same search in a browser.

Read the documentation¶

The Mathlib documentation lists every definition and lemma by file. Browsing the file for a concept, such as the one on ordered fields, is often the fastest way to learn what exists nearby.