Bundled `lift` for `free_group`

Stream: maths

[Yury G. Kudryashov]

I created a branch https://github.com/leanprover-community/mathlib/tree/free-group-lift with free_group.lift (former to_group) using bundled homs.

[Yury G. Kudryashov]

Help in fixing other files is very welcome but we need to coordinate.

[Yury G. Kudryashov]

I fixed up to free_abelian_group and tensor_product.

[Yury G. Kudryashov]

I've also defined free_abelian_group.ring_lift with plans to use free_monoid.lift.trans free_abelian_group.ring_lift as free_ring.lift.

[Yury G. Kudryashov]

(not done yet).

[Yury G. Kudryashov]

Unfortunately, this will lead to a large PR that can't be broken in smaller pieces.