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.

Estimated changes