Easy way to lift the entire structure?

Stream: new members

[Joe]

I have some algebraic structure, say a vector space. Then I take a quotient on the structure, and the equivalence relation is respected by all the operations of the algebraic structure (like addition and scalar multiplication). Then I want to say that the quotient space has the same algebraic structure, and there is a natural homomorphism between the original space and the quotient space. Do I need to prove everything again?

[Patrick Massot]

Currently we don't have a tactic automating this. But there are many examples in mathlib (including the one of vector spaces).