RFC: do not unfold semireducible definitions by default

[fpvandoorn]

I think aesop (and all other automation) should apply lemmas up to instances transparency by default. Otherwise, I don't think it is possible to make performant automation.
It is unreasonable to expect automation to be quick if it can unfold almost any definitions, and experimentally, sometimes apply ... takes seconds to fail (even if the lemma "obviously" doesn't apply). Sure, in those cases we could do better in Mathlib, marking more things irreducible, but we cannot only fix in on Mathlib's side.

My experience is that aesop is often very slow, and there have been multiple PRs to Mathlib moving away from aesop because of performance reasons: 1 2 3 4.

This will lead to a regression in capabilities of aesop and we will need to mark more things as unfoldable by aesop. Maybe specialized tactics like aesop_cat can work up to semireducible transparency.

I think I already talked to @JLimperg about this in person, but I'm surprised that I never wrote up the suggestion on Zulip/Github.

[JLimperg]

Thanks for bringing this up! Link to Zulip discussion for reference: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/should.20aesop.20unfold.20semireducible.20definitions.3F