S - {x} ?

Stream: Is there code for X?

[Kevin Buzzard]

Say S : set X. We have S.insert x for adding an element to S (i.e. a shortcut for S.union {x}); is there a corresponding function for S.diff {x}?

I would love to use #find to answer this kind of question myself; do I remember correctly that this is on the table for Lean 4?

[Yaël Dillies]

We have docs#finset.erase but not docs#set.erase

[Eric Wieser]

Presumably #find or library_search work fine in lean 3, but both suggest set.insert as it had the same type?

[Kevin Buzzard]

Sure, I don't mind something suggesting set.insert and a couple of other things; what I don't like is only being able to do #find set _ -> _ -> set _ which can be unified in far more ways than set X -> X -> set X (e.g. set.image, set.preimage etc)

[Eric Wieser]

Does #find Π X, set X → X → set X work?

[Kevin Buzzard]

It didn't when I tried variants of this idea

[Eric Wieser]

I was surprised to find out that docs#find_cmd is mathlib not core

[Joachim Breitner]

TIL! Maybe someone who knows this command well wants to respond to https://proofassistants.stackexchange.com/questions/354/how-to-search-for-an-existing-theorem-in-lean talking about it?

Can I use it to seach for lemmas that mention too anywhere in their type, potentially using

#find (_ foo)