Commit 2025-06-23 07:20 f5e444c2

View on Github →

chore(Algebra): replace messy simps! with Aesop lemmas, add a test (#26127)

  • Replace messy simps! auto-generated lemma unfolding .coe StarAlgebra.adjoin with an Aesop lemma
  • Add analogous Aesop lemmas for the other *Algebra.adjoin operations
  • Add analogous Aesop test for Algebra.adjoin The simps! lemma I have removed was necessary for an Aesop test in MathlibTest/set_like.lean to pass. With these changes, the test passes 7x faster. I have added an analogous test for Algebra.adjoin - before this PR Aesop was unable to prove membership of Algebra.adjoin, even though it could prove membership of StarAlgebra.adjoin (thanks to the simps! lemma). I intend to add analogous Aesop lemmas for the other substructure closure operators in a subsequent PR (edit: #26162) PR split from #25961

Estimated changes