library_search failing to apply symm

Stream: mathlib4

[David Renshaw]

library_search fails here:

lemma prime_of_prime (n : ℕ) : Prime n ↔ Nat.Prime n := by
  library_search

I expect it to find exact Nat.prime_iff.symm. In mathlib3, it does succeed at finding that.

Is this a bug in library_search?

[Alex J. Best]

Does rewrites do it? I'm not sure what we consider in scope for library search now that that exists also

[Scott Morrison]

I did change how library_search handles the symm versions of lemmas between mathlib3 and mathlib4, so this is likely a regression.

[David Renshaw]

rewrites gives me an error

Messages here (1)
18:2:
unknown constant 'irreducible_iff_prime_of_exists_unique_irreducible_factors'

[Scott Morrison]

Oh, that is definitely a bug, where rewrites is trying to use a lemma that hasn't been imported yet!

[Scott Morrison]

(which it knows about because of the global cache generated by CI)

[Scott Morrison]

Okay, the original problem is solved in !4#4534. Still looking at the error from rewrites.

[Scott Morrison]

The error from rewrites is fixed in !4#4537, which also results in

lemma prime_of_prime (n : ℕ) : Prime n ↔ Nat.Prime n := by
  rewrites!

closing the goal.