library_search has been merged

Stream: general

[Scott Morrison]

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]

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]

Hooray! This is awesome!

[Patrick Massot]

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

[Patrick Massot]

The goal was 1 ∈ ker φ

[Patrick Massot]

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

[Kevin Buzzard]

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.