-- 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_1 : IsFreeGroup.Generators G) ↦
          HSMul.hSMul (β := A) (IsFreeGroup.of e_1)
              (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'
refine_1 :
  ∀ (g : G), SemidirectProduct.right (N := A → X) (φ := mulAutArrow) ((F' : (a : G) → (A → X) ⋊[mulAutArrow] G) g) = g
refine_2 :
  (fun (F : ActionCategory G A ⥤ CategoryTheory.SingleObj X) ↦
      ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
        F.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)
    (uncurry F' ⋯)
refine_3 :
  ∀ (y : ActionCategory G A ⥤ CategoryTheory.SingleObj X),
    (fun (F : ActionCategory G A ⥤ CategoryTheory.SingleObj X) ↦
          ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
            F.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)
        y →
      y = uncurry F' ⋯
⊢ ∃! F : ActionCategory G A ⥤ CategoryTheory.SingleObj X,
    ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
      F.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

Tactic:
refine ⟨uncurry F' ?_, ?_, ?_⟩