I use three strategies to find existing lemmas: the
exact? tactic, the
gptf tactic and guessing the name based on mathlib naming conventions.
exact? is a mathlib tactic, not a Lean tactic. (It was earlier called
library_search.) It tries to find a single lemma from the library to solve the current goal, also using local hypotheses to fill in arguments. To make the best use of this tactic, make sure that:
- The current context doesn't have many extraneous assumptions. You might want to use the
clear and the
clear_except tactic to remove unnecessary assumptions. If you don't do this,
exact? might timeout.
- You have introduced all necessary variables and hypotheses. If your goal has forall and imply then it's very likely that
library_search won't be able to find anything.
- The assumptions are in
simp normal form.
exact? will only succeed if it can close the goal. If you would also like candidate incomplete solutions (i.e. where a library lemma can be applied to the goal, but then that lemma has hypotheses that can not be filled from the local context) then use
- There is now a relative of
apply? for rewriting, called
rw?, which will try to rewrite the current goal by a single lemma from the library, returning multiple candidates if none close the goal.
Unfortunately, this tactic is no longer a thing.
This tactic uses artificial intelligence. It is faster than
library_search, and sometimes smarter. When you are stuck, sometimes
gptf can give helpful hints. In addition to finding mathlib lemmas, sometimes
gptf can suggest tactics and complete proofs.
Follow the instructions on GitHub to get access to this tactic.
mathlib naming conventions
Please familiarize yourself with the naming conventions. You can often find lemmas by guessing its name and letting autocomplete help you.