#find gives bogus results

Here is a MWE:

import Lean
import Mathlib.Tactic.Find
import Mathlib.Data.Nat.Log

open Lean Parsec



#find  (_ - (_- _)) = _ + _ - _ 

This prints the following set of results

Equiv.punitEquivPUnit.proof_2: ∀ (x : PUnit), (fun x => PUnit.unit) ((fun x => PUnit.unit) x) = xLean 4
Function.Embedding.punit.proof_1: ∀ {β : Sort ?u.32685} (b : β) ⦃a₁ a₂ : PUnit⦄,
  (fun x => b) a₁ = (fun x => b) a₂ → a₁ = a₂Lean 4
PUnit.inf_eq: ∀ (a b : PUnit), a ⊓ b = PUnit.unitLean 4
PUnit.unique.proof_1: ∀ (x : PUnit), x = defaultLean 4
sub_sub_eq_add_sub: ∀ {α : Type ?u.118585} [inst : SubtractionMonoid α] (a b c : α), a - (b - c) = a + c - bLean 4
PUnit.hnot_eq: ∀ (a : PUnit), ￢a = PUnit.unitLean 4
PUnit.booleanAlgebra.proof_7: ∀ (x_1 y_1 : PUnit), x_1 ⇨ x_1 = y_1 ⊔ PUnit.unitLean 4
PUnit.default_eq_unit: default = PUnit.unitLean 4
PUnit.subsingleton: ∀ (a b : PUnit), a = bLean 4
PUnit.biheytingAlgebra.proof_10: ∀ (x : PUnit), x ⇨ ⊥ = x ⇨ ⊥Lean 4
PUnit.compl_eq: ∀ (a : PUnit), aᶜ = PUnit.unitLean 4
PUnit.sdiff_eq: ∀ (a b : PUnit), a \ b = PUnit.unitLean 4
PUnit.eq_punit: ∀ (a : PUnit), a = PUnit.unitLean 4
PUnit.min_eq: ∀ (a b : PUnit) {star : PUnit}, min a b = starLean 4
PUnit.sup_eq: ∀ (a b : PUnit), a ⊔ b = PUnit.unitLean 4
Unit.ext: ∀ (x y : Unit), x = yLean 4
PUnit.linearOrder.proof_7: ∀ (a b : PUnit), min a b = min a bLean 4
sub_sub_sub_eq: ∀ {α : Type ?u.305231} [inst : SubtractionCommMonoid α] (a b c d : α), a - b - (c - d) = a + d - (b + c)Lean 4
PUnit.max_eq: ∀ (a b : PUnit) {star : PUnit}, max a b = starLean 4
Equiv.punitEquivPUnit.proof_1: ∀ (x : PUnit), (fun x => PUnit.unit) ((fun x => PUnit.unit) x) = xLean 4
maximum number of search results reachedLean 4

Almost all the results do not match the query, but a couple of results which do match the query are sprinkled in among them. It is also unclear how many matching results are hidden due to the maximum number of search results being reached.

In general the PUnit lemmas pollute most #find results. There are also similar problems with library_search, but I'm not sure it's the same problem.

Start with the #find entry point from Mathlib.Tactic.Find and reproduce the provided MWE in Lean 4. Compare the reported matches with the query, including the PUnit lemmas and maximum-results behavior; done means unrelated results no longer pollute the output and matching results remain discoverable.