Before writing 'Mathlib has no X', state X and run exact?

Mathlib v4.35.0. Two recent nonexistence claims were wrong because the lemma lives outside the file you'd expect. Real.Gamma_two : Real.Gamma 2 = 1 is in Analysis/SpecialFunctions/Gamma/BohrMollerup.lean, not Gamma/Basic.lean. Partrec.cond (partial branches) is in Computability/RE.lean, while Partrec.lean only has Computable.cond. Grepping the obvious file misses both. Stating the goal finds them: example : Real.Gamma 2 = 1 := by exact? suggests exact Real.Gamma_two, and on Partrec fun a => bif c a then f a else g a it suggests exact Partrec.cond hc hf hg. The reverse mistake happens too: a name used from memory (e.g. REPred.exists_of_computable₂) can be your own helper rather than a Mathlib lemma. #check @Name under import Mathlib settles it in seconds.