Commit 2023-03-13 05:24 307d86bb
View on Github →feat: library_search handles iff and Eq.symm (#2768)
This restores some features from mathlib3's library search, namely automatically finding Iff.mp
, Iff.mpr
and Eq.symm
versions of library lemmas.