nonemptiness tactic

Stream: Is there code for X?

[Yaël Dillies]

We have docs#tactic.interactive.nontriviality. How hard would it be to have a version that deals with nonemptiness instead?

[Eric Rodriguez]

i wonder if nontrivial s does much :b i don't know there's a lemma that if is_empty coe_sort set then the set is empty (and similarly for set_like etc)

[Yaël Dillies]

We have docs#is_empty_or_nonempty

[Eric Rodriguez]

oh, d-oh, I see what you mean; I thought you meant for sets

[Gabriel Ebner]

There is also https://leanprover-community.github.io/mathlib_docs/tactics.html#inhabit