## Stream: general

### Topic: library_search has been merged

#### Scott Morrison (Mar 29 2019 at 03:36):

library_search is now available on master:

import tactic.interactive

example (a b : ℕ) (h : a ∣ b) (w : b > 0) : a ≤ b :=
by library_search -- says: exact nat.le_of_dvd w h

example {a b c : ℕ} (h₁ : a ∣ c) (h₂ : a ∣ b + c) : a ∣ b :=
by library_search -- says exact (nat.dvd_add_left h₁).mp h₂


#### Scott Morrison (Mar 29 2019 at 03:37):

Please try it out, and report any unexpected failures. It "should" work on any goal which can be closed by applying exactly one lemma from the currently imported library, then some sequence of applying local hypotheses.

#### Johan Commelin (Mar 29 2019 at 07:20):

Hooray! This is awesome!

#### Patrick Massot (Apr 03 2019 at 19:59):

I just used library_search for the first time. I feel so much smarter than one minute ago...

#### Patrick Massot (Apr 03 2019 at 19:59):

The goal was 1 ∈ ker φ

#### Patrick Massot (Apr 03 2019 at 20:09):

I did it again. I think I'm only a couple of uses away from being addicted.

#### Kevin Buzzard (Apr 03 2019 at 20:20):

I know this is kind of funny, but library_search is a big deal for people like me who don't seem to be able to instantly name every lemma in mathlib.

Last updated: May 12 2021 at 23:13 UTC