the tactic is called `admit' because you're admitting that you don't know how to complete the proof
https://thenewleafjournal.com/how-to-find-substack-rss-feeds-and-other-notes/ retvurn to RSS (which substack does at /feed that's nice)
This is just an alias for `admit`, but that's way less fun than just going `give_up` in a proof you're finding too difficult
Moved to @TetraspaceGrouping