how to find lemmas?

Stream: new members

[rzeta0]

I was thinking about this simple task:

$$x^2 = 0 \implies x = 0 \text { for } x \in \mathbb{R}$$

I started writing a lean proof ..

import Mathlib.Tactic

example {x : ℝ} (h: x^2 = 0) : x = 0 := by

... when I realised I have no clue how to search for and find relevant lemmas (such as eq_zero_or_eq_zero_of_mul_eq_zero).

Question: What is the recommended way to search for lemmas that might be useful to the task at hand?

The one's I have come across thus far (Heather Macbeth's course) are introduced by the author with the intention to be used in the examples and exercises.

[Martin Dvořák]

Tactics: exact? apply? rw? simp? aesop?
Online tools: Moogle, Loogle
Best thing ever: YaëlSearch (accessible via Zulip)

[jsodd]

Also this https://huggingface.co/spaces/dx2102/search-mathlib and this https://leansearch.net/

[Daniel Weber]

It's also useful to know the #naming convention, you can often guess lemma names

[Joachim Breitner]

Also very useful :
Jireh Loreaux said:

I gave a talk on exactly this topic at LftCM 2024 at CIRM. It was recorded and the video is here: https://library.cirm-math.fr/Record.htm?idlist=1&record=19392446124911106289