-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Goal:
G A : Type u
inst : Group G
inst_1 : IsFreeGroup G
inst_2 : MulAction G A
X : Type u
inst_3 : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun (e : IsFreeGroup.Generators G) ↦
    ⟨fun (b : A) ↦
      f (a :=
        Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
          ((IsFreeGroup.of e)⁻¹ • b))
        (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b)
        (Subtype.mk (p := fun (e_2 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_2)
              (ActionCategory.back (M := G)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                  ((IsFreeGroup.of e)⁻¹ • b))) =
            ActionCategory.back (M := G)
              (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () b))
          e ⋯),
      IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), (F' : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun (F : G →* (A → X) ⋊[mulAutArrow] G) ↦
          ∀ (a : IsFreeGroup.Generators G), (F : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a)
        y →
      y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE :
  ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
    E.map
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this := a;
                  this) ⟶
                b.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (actionAsFunctor G A) f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((actionAsFunctor G A).obj
                        (have this := a;
                          this).fst)) →
                  (fun (X : Type u) ↦ X) ((actionAsFunctor G A).obj b.fst))
              (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                (have this := a;
                this)) =
            b.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c))
          (IsFreeGroup.of (↑g : IsFreeGroup.Generators G)) ⋯) =
      f g
e : IsFreeGroup.Generators G
x : A
e_1 :
  X =
    (E.obj
        (have this : ActionCategory G A :=
          Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
            ((IsFreeGroup.of e)⁻¹ • x);
        this) ⟶
      E.obj (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () x))
⊢ Eq (α := X)
    (SemidirectProduct.left (G := G) (φ := mulAutArrow)
        ((curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e)) x :
      X)
    (E.map
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this : ActionCategory G A :=
                    Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                      ((IsFreeGroup.of e)⁻¹ • x);
                  this) ⟶
                Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () x)) ↦
          Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (actionAsFunctor G A)
                (Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () x))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (actionAsFunctor G A) f) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((actionAsFunctor G A).obj
                          (have this := ⟨(), (IsFreeGroup.of e)⁻¹ • x⟩;
                            this).fst)) →
                    (fun (X : Type u) ↦ X) ((actionAsFunctor G A).obj ⟨(), x⟩.fst))
                (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (have this : ActionCategory G A :=
                    Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                      ((IsFreeGroup.of e)⁻¹ • x);
                  this)) :
              (fun (X : Type u) ↦ X)
                (Functor.obj (actionAsFunctor G A)
                  (Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                    (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () x))))
            (Sigma.snd (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () x) :
              Functor.obj (actionAsFunctor G A)
                (Sigma.fst (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                  (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () x))))
          (IsFreeGroup.of
            (↑(Subtype.mk (p := fun (e_2 : IsFreeGroup.Generators G) ↦
                  HSMul.hSMul (β := A) (IsFreeGroup.of e_2)
                      (ActionCategory.back (M := G)
                        (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
                          ((IsFreeGroup.of e)⁻¹ • x))) =
                    ActionCategory.back (M := G)
                      (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () x))
                  e ⋯) :
              IsFreeGroup.Generators G))
          ⋯) :
      E.obj
          (have this : ActionCategory G A :=
            Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) ()
              ((IsFreeGroup.of e)⁻¹ • x);
          this) ⟶
        E.obj (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) () x))

Tactic:
rfl