Commit 2025-07-15 08:10 42d7516d

feat(Aesop): Improve SetLike ruleset (#25961)

• Make some Aesop rules in the SetLike ruleset unsafe
• Register new rules with the Aesop SetLike ruleset, by analogy with existing ones
  • Add new rules like mem_closure_of_mem by analogy with #26162 to improve performance in proving membership of closures. Before this PR, to prove something like x ∈ s ⊢ x ∈ closure s, Aesop would have to try the rule mem_of_subset, creating a metavariable that it would then try to fill with subset_closure . Obviously this was pretty inefficient, and the new lemma mem_closure_of_mem is a much more usable Aesop rule.
• Update some Aesop rules' probabilities
• Add new library note [SetLike Aesop ruleset] explaining the principles behind the new design The design note stipulates that safe-phase Aesop rules are to also be simp rules; this change has been split into #26175