where aesop is discouraged

Stream: mathlib4

[Elif Uskuplu]

Are there situations where aesop is discouraged in Mathlib PRs even if it closes the goal? For example, are there cases where reviewers would prefer simp, exact, omega, or a more explicit proof over a working aesop call? I'm curious about both style conventions and practical concerns like compile time.

[Eric Wieser]

For a single line proof, it is often much better to use exact as that make it clearer what refactors are possible.

[Monica Omar]

if simp or simp_all can do the job, then that's better than aesop

[Violeta Hernández]

In my experience grind can solve a lot of the same goals aesop can, and when it does it's often noticeably faster.

[Edward van de Meent]

in my cayley graph PR (#35084) both mulCayley_adj and mulCayley_eq_erase_one are solved by aesop but not grind after unfolding the definition... i wonder why

[Vlad Tsyrklevich]

in mulCayley_adj, try? succeeds after simp and simp? shows that the missing lemma is fromRel_adj (e.g. unfold mulCayley; grind [fromRel_adj, eq_inv_mul_iff_mul_eq] succeeds.)

For the second I only got it work with an intermediate simp and I am at the edge of my grind knowledge to say more

  unfold mulCayley
  simp only [fromRel, Set.mem_diff]
  grind [mul_one]