mathlib

1d5b99b2 - feat(group_theory/free_product): add (m)range_eq_supr (#12956)

feat(group_theory/free_product): add (m)range_eq_supr (#12956) and lemmas leading to it as inspired by the corresponding lemmas from `free_groups.lean`. As suggested by @ocfnash, polish the free group lemmas a bit as well.