mathlib

3894503e - doc(tactic/library_search): use more detailed doc string in docs (#5206)

doc(tactic/library_search): use more detailed doc string in docs (#5206) The doc string for `tactic.interactive.library_search` is better than the tactic doc entry. The latter is missing details like `library_search!` Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>