mathlib3

7ae2af63 - feat(group_theory/is_free_group): promote `is_free_group.lift'` to an equiv (#7110)

feat(group_theory/is_free_group): promote `is_free_group.lift'` to an equiv (#7110) While non-computable, this makes the API of `is_free_group` align more closely with `free_group`. Based on discussion in the original PR, this doesn't go as far as changing the definition of `is_free_group` to take the equiv directly. This additionally: * adds the definition `lift`, a universe polymorphic version of `lift'` * adds the lemmas: * `lift'_eq_free_group_lift` * `lift_eq_free_group_lift` * `of_eq_free_group_of` * `ext_hom'` * `ext_hom` * renames `is_free_group.iso_free_group_of_is_free_group` to the shorter `is_free_group.to_free_group` * removes lemmas absent from the `free_group` API that are no longer needed for the proofs here: * `end_is_id` * `eq_lift`