Iff not

Stream: Is there code for X?

[Marcus Rossel]

Does the following lemma not exist (in mathlib 4)?:

example (p q : Prop) : (p ↔ q) ↔ (¬p ↔ ¬q) := ...

Library search couldn't find it.

[Yaël Dillies]

docs4#not_iff_not ?

[Eric Wieser]

docs#iff.not docs4#Iff.not :point_up:

[Marcus Rossel]

Thanks! I guess library search (for mathlib 4) isn't quite ready yet?

[Yaël Dillies]

What does example (p q : Prop) : (¬ p ↔ ¬ q) ↔ (p ↔ q) := by library_search do?

[Marcus Rossel]

That works

[Kevin Buzzard]

I guess the rule of thumb is "more complex expression on the left hand side" but even so I thought that lean 3 library search would have got it

[Eric Wieser]

I think lean3 library search does, but this is Lean 4

[Scott Morrison]

Interesting, I thought I had fixed Lean4's library_search to find the symmetric versions of lemmas. I created https://github.com/leanprover-community/mathlib4/issues/3426 to track library_search issues, and anyone should feel free to contribute examples that should work there.