mathlib3

d9dc30e5 - feat(algebra/free): turn `free_magma.lift` into an equivalence (#6672)

feat(algebra/free): turn `free_magma.lift` into an equivalence (#6672) This will be convenient for some work I have in mind and is more consistent with the pattern used elsewhere, such as: - [`free_algebra.lift`](https://leanprover-community.github.io/mathlib_docs/algebra/free_algebra.html#free_algebra.lift) - [`monoid_algebra.lift`](https://leanprover-community.github.io/mathlib_docs/algebra/monoid_algebra.html#monoid_algebra.lift) - [`universal_enveloping.lift`](https://leanprover-community.github.io/mathlib_docs/algebra/lie/universal_enveloping.html#universal_enveloping_algebra.lift) - ...