awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
G : Type u_3
inst : Group G
b : FreeGroupBasis ι G
i : ι
change : (b.repr : (a : G) → FreeGroup ι) ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i)) = FreeGroup.of i
⊢ (b.repr : (a : G) → FreeGroup ι) ((b : (a : ι) → G) i) = FreeGroup.of i

Tactic:
change b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i

Premises used: FreeGroup.of, FreeGroupBasis.repr, MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
G : Type u_3
inst : Group G
b : FreeGroupBasis ι G
i : ι
⊢ (b.repr : (a : G) → FreeGroup ι) ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i)) = FreeGroup.of i

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
X : Type u_5
x : X
⊢ (ofFreeGroup X : (a : X) → FreeGroup X) x = FreeGroup.of x

Tactic:
rfl

Premises used: FreeGroup.of, FreeGroup.mk, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
inst : Group G
b : FreeGroupBasis ι G
e : ι ≃ ι'
x : ι'
⊢ Eq.{u_3 + 1} (α := G) ((b.reindex e : (a : ι') → G) x : G) ((b : (a : ι) → G) ((e.symm : (a : ι') → ι) x : ι) : G)

Tactic:
rfl

Premises used: FreeGroup.of, List.map, FreeGroup.mk, Quot.map, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b : FreeGroupBasis ι G
e : G ≃* H
x : ι
⊢ Eq.{u_4 + 1} (α := H) ((b.map e : (a : ι) → H) x : H) ((e : (a : G) → H) ((b : (a : ι) → G) x : G) : H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
G : Type u_3
inst : Group G
b : FreeGroupBasis ι G
⊢ Injective.{u_1 + 1, u_3 + 1} (α := ι) (β := G) (⇑b : (a : ι) → G)

Tactic:
b.repr.symm.injective.comp FreeGroup.of_injective

Premises used: FreeGroupBasis.repr, Function.Injective.comp, FreeGroup.of_injective, MulEquiv.symm, MulEquiv.injective
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
G : Type u_3
inst : Group G
b : FreeGroupBasis ι G
⊢ IsFreeGroup G

Tactic:
⟨range b, ⟨b.reindex (Equiv.ofInjective (↑b) b.injective)⟩⟩

Premises used: FreeGroupBasis.injective, Set.Elem, IsFreeGroup.mk, Nonempty.intro, Equiv.ofInjective, Exists.intro, Set.range, FreeGroupBasis.reindex, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
X : Type u_5
⊢ IsFreeGroup.{u_5} (FreeGroup X)

Tactic:
(ofFreeGroup X).isFreeGroup

Premises used: FreeGroupBasis.isFreeGroup, FreeGroupBasis.ofFreeGroup
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b : FreeGroupBasis ι G
f : MonoidHom.{u_1, u_4} (FreeGroup ι) H
h :
  ∀ (a : ι),
    Eq.{u_4 + 1} (α := H)
      (((fun (f : G →* H) ↦ f.comp b.repr.symm.toMonoidHom)
              ((fun (f : MonoidHom.{u_1, u_4} (FreeGroup ι) H) ↦ f.comp b.repr.toMonoidHom) f) :
            (a : FreeGroup ι) → H)
          (FreeGroup.of a) :
        H)
      ((f : (a : FreeGroup ι) → H) (FreeGroup.of a) : H)
⊢ (fun (f : G →* H) ↦ f.comp b.repr.symm.toMonoidHom)
      ((fun (f : MonoidHom.{u_1, u_4} (FreeGroup ι) H) ↦ f.comp b.repr.toMonoidHom) f) =
    f

Tactic:
ext
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b : FreeGroupBasis ι G
f : MonoidHom.{u_1, u_4} (FreeGroup ι) H
a : ι
⊢ Eq.{u_4 + 1} (α := H)
    (((fun (f : G →* H) ↦ f.comp b.repr.symm.toMonoidHom)
            ((fun (f : MonoidHom.{u_1, u_4} (FreeGroup ι) H) ↦ f.comp b.repr.toMonoidHom) f) :
          (a : FreeGroup ι) → H)
        (FreeGroup.of a) :
      H)
    ((f : (a : FreeGroup ι) → H) (FreeGroup.of a) : H)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b : FreeGroupBasis ι G
f : G →* H
h :
  ∀ (x : G),
    Eq.{u_4 + 1} (α := H)
      (((fun (f : MonoidHom.{u_1, u_4} (FreeGroup ι) H) ↦ f.comp b.repr.toMonoidHom)
              ((fun (f : G →* H) ↦ f.comp b.repr.symm.toMonoidHom) f) :
            (a : G) → H)
          x :
        H)
      ((f : (a : G) → H) x : H)
⊢ (fun (f : MonoidHom.{u_1, u_4} (FreeGroup ι) H) ↦ f.comp b.repr.toMonoidHom)
      ((fun (f : G →* H) ↦ f.comp b.repr.symm.toMonoidHom) f) =
    f

Tactic:
ext
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b : FreeGroupBasis ι G
f : G →* H
x : G
⊢ Eq.{u_4 + 1} (α := H)
    (((fun (f : MonoidHom.{u_1, u_4} (FreeGroup ι) H) ↦ f.comp b.repr.toMonoidHom)
            ((fun (f : G →* H) ↦ f.comp b.repr.symm.toMonoidHom) f) :
          (a : G) → H)
        x :
      H)
    ((f : (a : G) → H) x : H)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
G : Type u_3
H : Type u_4
inst : Group G
inst_1 : Group H
b : FreeGroupBasis ι G
f g : G →* H
h :
  ∀ (i : ι),
    Eq.{u_4 + 1} (α := H) ((f : (a : G) → H) ((b : (a : ι) → G) i : G) : H)
      ((g : (a : G) → H) ((b : (a : ι) → G) i : G) : H)
⊢ f = g

Tactic:
b.lift.symm.injective <| funext h

Premises used: FreeGroupBasis.lift, funext, Equiv.injective, Equiv.symm
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G_1 : Type u_3
H : Type u_4
inst : Group G_1
inst_1 : Group H
G : Type u
inst_2 : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of :
  ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X),
    (((lift : (a : X → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a
h :
  ∀ (a : X),
    Eq (α := FreeGroup X)
      ((MonoidHom.comp (N := G) ((lift : (a : X → FreeGroup X) → G →* FreeGroup X) FreeGroup.of)
              ((FreeGroup.lift : (a : X → G) → FreeGroup X →* G) of) :
            (a : FreeGroup X) → FreeGroup X)
          (FreeGroup.of a) :
        FreeGroup X)
      ((MonoidHom.id (FreeGroup X) : (a : FreeGroup X) → FreeGroup X) (FreeGroup.of a) : FreeGroup X)
⊢ Eq.{u + 1} (α := FreeGroup X →* FreeGroup X)
    (MonoidHom.comp (N := G) ((lift : (a : X → FreeGroup X) → G →* FreeGroup X) FreeGroup.of)
      ((FreeGroup.lift : (a : X → G) → FreeGroup X →* G) of))
    (MonoidHom.id (FreeGroup X))

Tactic:
apply FreeGroup.ext_hom

Premises used: FreeGroup.ext_hom
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G_1 : Type u_3
H : Type u_4
inst : Group G_1
inst_1 : Group H
G : Type u
inst_2 : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of :
  ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X),
    (((lift : (a : X → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a
x : X
⊢ Eq (α := FreeGroup X)
    ((MonoidHom.comp (N := G) ((lift : (a : X → FreeGroup X) → G →* FreeGroup X) FreeGroup.of)
            ((FreeGroup.lift : (a : X → G) → FreeGroup X →* G) of) :
          (a : FreeGroup X) → FreeGroup X)
        (FreeGroup.of x) :
      FreeGroup X)
    ((MonoidHom.id (FreeGroup X) : (a : FreeGroup X) → FreeGroup X) (FreeGroup.of x) : FreeGroup X)

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply,
          FreeGroup.lift_apply_of, lift_of]

Premises used: MonoidHom.coe_comp, FreeGroup.lift_apply_of, MonoidHom.id_apply, Function.comp_apply
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G_1 : Type u_3
H_1 : Type u_4
inst : Group G_1
inst_1 : Group H_1
G : Type u
inst_2 : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of :
  ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X),
    (((lift : (a : X → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a
H : Type u
_ :
  ∀ [inst : Group H] (f : G →* H) (a : X),
    Eq.{u + 1} (α := H) ((Equiv.symm lift : (a : G →* H) → X → H) f a : H) ((f : (a : G) → H) (of a) : H)
⊢ ∀ [inst : Group H] (f : G →* H) (a : X),
    Eq.{u + 1} (α := H) ((Equiv.symm lift : (a : G →* H) → X → H) f a : H) ((f : (a : G) → H) (of a) : H)

Tactic:
_
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G_1 : Type u_3
H_1 : Type u_4
inst : Group G_1
inst_1 : Group H_1
G : Type u
inst_2 : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of :
  ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X),
    (((lift : (a : X → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a
H : Type u
inst_3 : Group H
f : G →* H
a : X
⊢ Eq.{u + 1} (α := H) ((Equiv.symm lift : (a : G →* H) → X → H) f a : H) ((f : (a : G) → H) (of a) : H)

Tactic:
simp [← lift_of (lift.symm f)]

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G_1 : Type u_3
H : Type u_4
inst : Group G_1
inst_1 : Group H
G : Type u
inst_2 : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of :
  ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X),
    (((lift : (a : X → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X),
  Eq.{u + 1} (α := H) ((Equiv.symm lift : (a : G →* H) → X → H) f a : H) ((f : (a : G) → H) (of a) : H) :=
  ⋯
a :
  Eq.{u + 1} (α := X → G)
    ((Equiv.symm lift : (a : G →* G) → X → G)
        (MonoidHom.comp (N := FreeGroup X) ((FreeGroup.lift : (a : X → G) → FreeGroup X →* G) of)
          ((lift : (a : X → FreeGroup X) → G →* FreeGroup X) FreeGroup.of)) :
      X → G)
    ((Equiv.symm lift : (a : G →* G) → X → G) (MonoidHom.id G) : X → G)
⊢ Eq (α := G →* G)
    (MonoidHom.comp (N := FreeGroup X) ((FreeGroup.lift : (a : X → G) → FreeGroup X →* G) of)
      ((lift : (a : X → FreeGroup X) → G →* FreeGroup X) FreeGroup.of))
    (MonoidHom.id G)

Tactic:
apply lift.symm.injective

Premises used: Equiv.injective, Equiv.symm
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G_1 : Type u_3
H : Type u_4
inst : Group G_1
inst_1 : Group H
G : Type u
inst_2 : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of :
  ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X),
    (((lift : (a : X → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X),
  Eq.{u + 1} (α := H) ((Equiv.symm lift : (a : G →* H) → X → H) f a : H) ((f : (a : G) → H) (of a) : H) :=
  ⋯
a :
  ∀ (x : X),
    Eq.{u + 1} (α := G)
      ((Equiv.symm lift : (a : G →* G) → X → G)
          (MonoidHom.comp (N := FreeGroup X) ((FreeGroup.lift : (a : X → G) → FreeGroup X →* G) of)
            ((lift : (a : X → FreeGroup X) → G →* FreeGroup X) FreeGroup.of))
          x :
        G)
      ((Equiv.symm lift : (a : G →* G) → X → G) (MonoidHom.id G) x : G)
⊢ Eq.{u + 1} (α := X → G)
    ((Equiv.symm lift : (a : G →* G) → X → G)
        (MonoidHom.comp (N := FreeGroup X) ((FreeGroup.lift : (a : X → G) → FreeGroup X →* G) of)
          ((lift : (a : X → FreeGroup X) → G →* FreeGroup X) FreeGroup.of)) :
      X → G)
    ((Equiv.symm lift : (a : G →* G) → X → G) (MonoidHom.id G) : X → G)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
ι : Type u_1
ι' : Type u_2
G_1 : Type u_3
H : Type u_4
inst : Group G_1
inst_1 : Group H
G : Type u
inst_2 : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of :
  ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X),
    (((lift : (a : X → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X),
  Eq.{u + 1} (α := H) ((Equiv.symm lift : (a : G →* H) → X → H) f a : H) ((f : (a : G) → H) (of a) : H) :=
  ⋯
x : X
⊢ Eq.{u + 1} (α := G)
    ((Equiv.symm lift : (a : G →* G) → X → G)
        (MonoidHom.comp (N := FreeGroup X) ((FreeGroup.lift : (a : X → G) → FreeGroup X →* G) of)
          ((lift : (a : X → FreeGroup X) → G →* FreeGroup X) FreeGroup.of))
        x :
      G)
    ((Equiv.symm lift : (a : G →* G) → X → G) (MonoidHom.id G) x : G)

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply,
          FreeGroup.lift_apply_of, lift_of, lift_symm_of]

Premises used: MonoidHom.coe_comp, FreeGroup.lift_apply_of, MonoidHom.id_apply, Function.comp_apply
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : IsFreeGroup G
H : Type u_2
inst_2 : Group H
f : Generators G → H
a : Generators G
⊢ (((lift : (a : Generators G → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a

Tactic:
congr_fun (lift.symm_apply_apply f) a

Premises used: Equiv.symm_apply_apply, IsFreeGroup.lift, IsFreeGroup.of, congr_fun
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : IsFreeGroup G
H : Type u_2
inst_2 : Group H
f : G →* H
a : Generators G
⊢ Eq.{u_2 + 1} (α := H) ((Equiv.symm lift : (a : G →* H) → Generators G → H) f a : H) ((f : (a : G) → H) (of a) : H)

Tactic:
rfl

Premises used: IsFreeGroup.of, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : IsFreeGroup G
H : Type u_2
inst_2 : Group H
f g : G →* H
h : ∀ (a : Generators G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) (of a) : H) ((g : (a : G) → H) (of a) : H)
⊢ f = g

Tactic:
lift.symm.injective (funext h)

Premises used: IsFreeGroup.lift, funext, Equiv.injective, Equiv.symm
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : IsFreeGroup G
H : Type u_2
inst_2 : Group H
f : Generators G → H
⊢ ∃! F : G →* H, ∀ (a : Generators G), (F : (a : G) → H) (of a) = f a

Tactic:
simpa only [funext_iff] using lift.symm.bijective.existsUnique f

Premises used: Equiv.bijective, funext_iff, Function.Bijective.existsUnique, IsFreeGroup.lift, Equiv.symm
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
G : Type u
inst : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst_1 : Group H] → (X → H) ≃ (G →* H)
lift_of :
  ∀ {H : Type u} [inst_1 : Group H] (f : X → H) (a : X),
    (((lift : (a : X → H) → G →* H) f : G →* H) : (a : G) → H) (of a) = f a
⊢ IsFreeGroup G

Tactic:
(FreeGroupBasis.ofLift X of lift lift_of).isFreeGroup

Premises used: FreeGroupBasis.isFreeGroup, FreeGroupBasis.ofLift
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
G : Type u
inst : Group G
X : Type u
of : X → G
h : ∀ {H : Type u} [inst_1 : Group H] (f : X → H), ∃! F : G →* H, ∀ (a : X), (F : (a : G) → H) (of a) = f a
⊢ IsFreeGroup G

Tactic:
(FreeGroupBasis.ofUniqueLift X of h).isFreeGroup

Premises used: FreeGroupBasis.ofUniqueLift, FreeGroupBasis.isFreeGroup
-- Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : IsFreeGroup G
H : Type u_2
inst_2 : Group H
e : G ≃* H
⊢ IsFreeGroup H

Tactic:
((basis G).map e).isFreeGroup

Premises used: FreeGroupBasis.isFreeGroup, FreeGroupBasis.map, IsFreeGroup.basis
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
Goal:
G : Type u_1
inst : Groupoid.{v, u_1} G
inst_1 : IsFreeGroupoid.{v, u_1} G
X : Type v
inst_2 : Group X
f g : CategoryTheory.Functor.{v, v, u_1, 0} G (CategoryTheory.SingleObj X)
h : ∀ (a b : Generators.{u_1, v} G) (e : a ⟶ b), f.map (of e) = g.map (of e)
⊢ f = g

Tactic:
let ⟨_, _, u⟩ := @unique_lift G _ _ X _ fun (a b : Generators G) (e : a ⟶ b) => g.map (of e)
  _root_.trans (u _ h) (u _ fun _ _ _ => rfl).symm

Premises used: trans, _private.0.IsFreeGroupoid.ext_functor.match_1, CategoryTheory.Functor.map, IsFreeGroupoid.of, IsFreeGroupoid.unique_lift, Eq.symm, Eq, 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 : 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
⊢ ∀ [inst_3 : Group X] (f : Labelling (Generators (ActionCategory G A)) X),
    ∃! 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:
_
-- 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'
⊢ ∃! 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:
⟨uncurry F' ?_, ?_, ?_⟩

Premises used: CategoryTheory.ActionCategory.uncurry, ExistsUnique, And.intro, Exists.intro
-- 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:
DFunLike.ext_iff.mp this

Premises used: DFunLike.ext_iff, Iff.mp