awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
this : MonoidHom.comp SemidirectProduct.rightHom F' = MonoidHom.id G
⊢ ∀ (g : G), SemidirectProduct.right (N := A → X) (φ := mulAutArrow) ((F' : (a : G) → (A → X) ⋊[mulAutArrow] G) g) = g

Tactic:
exact DFunLike.ext_iff.mp this

Premises used: DFunLike.ext_iff, Iff.mp
-- 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 : MonoidHom.comp SemidirectProduct.rightHom F' = MonoidHom.id G
⊢ ∀ (g : G), SemidirectProduct.right (N := A → X) (φ := mulAutArrow) ((F' : (a : G) → (A → X) ⋊[mulAutArrow] G) g) = g

Tactic:
suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id _ by
        exact DFunLike.ext_iff.mp this
-- 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'
apply :
  ∀ (x : IsFreeGroup.Generators G),
    Eq (α := G) ((MonoidHom.comp SemidirectProduct.rightHom F' : (a : G) → G) (IsFreeGroup.of x) : G)
      ((MonoidHom.id G : (a : G) → G) (IsFreeGroup.of x) : G)
⊢ MonoidHom.comp SemidirectProduct.rightHom F' = MonoidHom.id G

Tactic:
apply IsFreeGroup.ext_hom (fun x ↦ ?_)

Premises used: IsFreeGroup.ext_hom
-- 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'
x : IsFreeGroup.Generators G
rw :
  Eq (α := G) ((SemidirectProduct.rightHom : (a : (A → X) ⋊[mulAutArrow] G) → G) (f' x) : G)
    ((MonoidHom.id G : (a : G) → G) (IsFreeGroup.of x) : G)
⊢ Eq (α := G) ((MonoidHom.comp SemidirectProduct.rightHom F' : (a : G) → G) (IsFreeGroup.of x) : G)
    ((MonoidHom.id G : (a : G) → G) (IsFreeGroup.of x) : G)

Tactic:
rw [MonoidHom.comp_apply, hF']

Premises used: MonoidHom.comp_apply
-- 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'
x : IsFreeGroup.Generators G
⊢ Eq (α := G) ((SemidirectProduct.rightHom : (a : (A → X) ⋊[mulAutArrow] G) → G) (f' x) : G)
    ((MonoidHom.id G : (a : G) → G) (IsFreeGroup.of x) : G)

Tactic:
rfl
-- 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'
b : Functor.obj (actionAsFunctor G A) PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b
⊢ (f'
          (↑(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)
                        PUnit.unit ((IsFreeGroup.of e)⁻¹ • b))) =
                  ActionCategory.back
                    (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c)
                      PUnit.unit b))
                e h) :
            IsFreeGroup.Generators G)).left
      (ActionCategory.back
        (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit b)) =
    f (a :=
      Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit
        ((IsFreeGroup.of e)⁻¹ • b))
      (b := Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit 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) PUnit.unit
                ((IsFreeGroup.of e)⁻¹ • b))) =
          ActionCategory.back
            (Sigma.mk (β := fun (c : CategoryTheory.SingleObj G) ↦ Functor.obj (actionAsFunctor G A) c) PUnit.unit b))
        e h)

Tactic:
rfl
-- 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'
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
a : ∀ (a : IsFreeGroup.Generators G), (curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
⊢ curry E = F'

Tactic:
apply uF'
-- 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'
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
a :
  ∀ (x : A),
    SemidirectProduct.left (G := G) (φ := mulAutArrow)
        ((curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e)) x =
      (f' e).left x
a₁ :
  SemidirectProduct.right (N := A → X) (φ := mulAutArrow)
      ((curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e)) =
    (f' e).right
⊢ (curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e) = f' e

Tactic:
ext
-- 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'
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
⊢ SemidirectProduct.right (N := A → X) (φ := mulAutArrow)
      ((curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e)) =
    (f' e).right

Tactic:
rfl
-- 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'
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
⊢ curry E = F'

Tactic:
have : curry E = F' := by
        apply uF'
        intro e
        ext
        · convert! hE _ _ _
          rfl
        · rfl