Commit 2023-04-12 19:26 74101a79

feat: @[eqns] attribute to override equation lemmas (#3024) This is to help with #2960 and work around https://github.com/leanprover/lean4/issues/2042. Ideally we would inspect the function to find that it was declared as | i, j => A j i and generate transpose_apply, but that's not something I know how to do.