mathlib

mathlib copied to clipboard

It would be nice to have a tactic that can transfer definitions and / or theorems through equivalences. E.g., all theorems in the upper half of data/equiv/algebra should be by equiv_transfer e.

In its simplest form it should assume that there is no structure on the target type, and transfer everything from the source type. I.e., it should analyze the requested type, and substitute e, e.symm, e.apply_symm_apply and e.symm_apply_apply as needed.

A more advanced version should be able to work with a target type that already has some structure but this structure agrees with that on the source type (e.g., e (a * b) = e a * e b), and the lemmas that prove these equalities either have predictable names, or are given as arguments to the tactic.

With the second type of tactic, it would be easy to define new types that are mathematically equivalent to old ones but provide better performance (more precisely, to prove theorems about these types).