[tachim]

There have been many contributions to mathlib from Aristotle already, it’s a major use case for our users