aesop appreciation thread

Stream: lean4

[David Renshaw]

@Jannis Limperg I just wanted to say: thank you for aesop. It's awesome. I used it this morning to significantly simplify some proofs:
https://github.com/dwrensha/math-puzzles-in-lean4/commit/92e73c025c5e5323b01188543d4b0b791506ceda
https://github.com/dwrensha/math-puzzles-in-lean4/commit/868b8effe24d4e302ed7bc1fd196341206069dbd

[Jannis Limperg]

Oh, thank you so much! I do love those diffs!

[Kevin Buzzard]

Using aesop is clearly cheating

[Wojciech Nawrocki]

I would also like to express my appreciation for aesop! It is possible to express various proofs as sequences of have : property₀ := by aesop; have : property₁ := by aesop; .., assuming sufficiently small jumps from propertyᵢ to propertyᵢ₊₁.