feat(GroupTheory/FreeGroup/Orbit): The orbit of a point generated by parts of a free group can be "duplicated"

[Bergschaf]

Applying w⁻¹ to the orbit generated by all elements of a free group that start with w yields
the orbit generated by all the words that start with every letter execpt w⁻ (and the original point)
The orbit of a point x generated by a set of group elements s defined as all the points that can be reached by applying the elements of s to x.
A special case of this result is needed for the banach tarski theorem.

---

I tried my best to shorten the proof of orbit.duplicate, but is quite long. There are some aspects that are duplicated due to case splits but I don't konw if it is possible to avoid that. I'd apprectiate some tips on that.
And I'm not quite sure about the naming of the theorems and definitions, please let me know if you have other (better) ideas!

[github-actions]

PR summary 9978e095d4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.GroupTheory.FreeGroup.Orbit (new file)	526

---

Declarations diff

+ Orbit.duplicate
+ instance {w : α × Bool} : SMul (startsWith w) X
+ startsWith
+ startsWith.ne_one
+ startsWith.neq_disjoint
+ startsWith.smul_def
+ startsWith_mk_mul
-++- mem_orbit_iff
-+-+ mem_orbit

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[tb65536]

Can you fix the build?

[tb65536]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by tb65536.

[adomani]

Hiding in here there seems to be a statement about injectivity of startsWith: would formulating such a statement simplify the arguments?

[Bergschaf]

I think this statement is a bit stronger, because it follows from a != b -> Disjoint (startsWith a) (startsWith b) not just from Injectivity.

[Bergschaf]

I pushed a fix that states this more clearly