obviously replacement in category theory

Stream: mathlib4

[Henrik Böving]

https://github.com/leanprover-community/mathlib4/pull/1287#issuecomment-1368547326

Can someone confirm this with a little more..certainty? :D

[Mario Carneiro]

it's a bit speculative at the moment, but yes this is the approach we are taking for uses of tidy and obviously in category theory

[Mario Carneiro]

aesop is a significantly different tactic than tidy, but it seems to work on similar goals. I'm not sure what we will do when there are discrepancies, but aesop is very configurable so maybe we can make it do what we want with enough annotations

[Adam Topaz]

We've been using aesop_cat so far, as far as I can tell

[Adam Topaz]

So yes what Joël wrote seems correct to me.

[Adam Topaz]

Take a look e.g. at docs4#CategoryTheory.Category vs docs#category_theory.category