Cateloguing different types of lemmas with attributes

Stream: PhysLean

[Joseph Tooby-Smith]

I am wondering if it is worth creating an attribute (or multiple) that can help catalogue different types of lemmas. I'm thinking of examples like:

• Equivariance under a group action.
• Invariance under a group action.
• Monotonicity
• Property reflection under a map
• Property preservation under a map
• Algebraic rewriting
• Integral calculation
• Derivative calculation

The idea would be to help people find lemmas of a given type, and maybe given them ideas on how to prove a result they are after.