library_search

Stream: lean4

[Henrik Böving]

Library search seems to be a little too smart here:
image.png :rolling_on_the_floor_laughing:
Is this intended?

[Henrik Böving]

Especially considering there is actually a lemma that solves this: iff_iff_and_or_not_and_not: ∀ {a b : Prop}, (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b

[Mauricio Collares]

I think this was fixed in https://github.com/leanprover-community/mathlib4/pull/239

[Arthur Paulino]

Does it still happen with the most recent version of Mathlib4? If so, please open an issue with a #mwe