List of domain specific tactics

Stream: new members

[Andy Jiang]

Hi is there a list of tactics in Lean written somewhere which is sorted by the area of its use? For example similar to omega for natural numbers but for other things.

More specifically currently I am looking for a tactic for lists which can resolve things like List.toFinset_replicate_of_ne_zero, or automatically construct functions List.toFinset (lst) = {p} -> p \in lst, etc. Does this exist?

Another one could be for basic number theory, encapsulating things like primes are >1; prime powers are >1; prime powers have a unique prime factor; etc

Sorry if I come across as asking for too much--it isn't my intention. I'm more curious what's available rather than making demands