Free Groups in Lean

Stream: general

[Christian K]

How can I create a Free Group of a custom inductive datatype in lean4?

inductive AB : Type u where
  | a
  | b

[Eric Wieser]

docs#FreeGroup, as FreeGroup AB

[Kevin Buzzard]

If you search the docs for free group (click "google site search") then you'll get led to this page from which you can deduce that the import is import Mathlib.GroupTheory.FreeGroup and you can then make the free group with FreeGroup AB.

[Christian K]

OK thanks, i tried using this Mathlib package before but i just got errors along the lines of "couldn*t construct instance of...." but now it works.
I looked into the FreeGroup.lean source file but i don't understand how i would prove, that a certain variable is an Element of this Free Group:

 import Mathlib.GroupTheory.FreeGroup

inductive AB : Type u where
  | a
  | b

variable (freegroup: Freegroup AB)


theorem a_in_freegroup(a : AB) : a ∈ freegroup := by
  sorry

But, more importantly, I want to prove that if i Take away the First Element of all Words that start with a, that I would get all the words that
start with a^-1, b and b^-1. How would a formulate this proof?

[Joachim Breitner]

Freegroup AB is the type of all (reduced) words in AB. So when you write freegroup: Freegroup AB, then freegroup isn’t the free group, but an arbitrary element of it.

[Joachim Breitner]

The canonical injection from the carrier type into the free group is docs#FreeGroup.of

[Joachim Breitner]

I am not sure how well the FreeGroup API is set up to talk about removing elements etc. You can use docs#FreeGroup.toWord to drop to a list of single elements.