library_search not finding obvious proof

Stream: lean4

[Jasmin Blanchette]

In the example below, library_search finds some weird spurious proofs:

import Mathlib.Algebra.Field.Defs
import Mathlib.Tactic.LibrarySearch

@[simp] theorem foo (x y : ℚ)
    (h : y ≠ 0) :
  x * y / y = x :=
  by
    library_search

In the next example, which is the same except for the imports, library_search fails to find the obvious proof that follows its call:

import Mathlib.Algebra.Field.Defs
import Mathlib.Tactic.LibrarySearch
import Mathlib.Tactic.Ring

@[simp] theorem foo (x y : ℚ)
    (h : y ≠ 0) :
  x * y / y = x :=
  by
    library_search
    apply mul_div_cancel
    apply h

[Jasmin Blanchette]

I'm using the mathlib4 from this morning.

[Ruben Van de Velde]

Also reported in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Proof.20automation/near/319928129

[Jasmin Blanchette]

The first half of my report is already reported. There remains the second half.

[Kevin Buzzard]

Seems that if library_search goes into this "print out 100 useless refinestatements" mode then it also closes the goal with sorry.

import Mathlib.Algebra.Field.Defs
import Mathlib.Tactic.LibrarySearch
import Mathlib.Tactic.Ring

-- remove y ≠ 0
@[simp] theorem foo (x y : ℚ) : x * y / y = x :=
  by
    library_search -- no errors and lots of noise in infoview

-- false
example : (3 : ℚ) * 0 / 0 = 3 := foo 3 0

and foo is highlighted as having been proved with sorry.