awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
⊢ b.symm = b'.symm
have h : ∀ (x : FreeGroup ι),
  Eq.{u_3 + 1} (α := G) ((b.symm : (a : FreeGroup ι) → G) x : G) ((b'.symm : (a : FreeGroup ι) → G) x : G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
⊢ { repr := b : FreeGroupBasis ι G } = { repr := b' }
have this : b.symm = b'.symm
Tactic: have : b.symm = b'.symm := by ext x; exact DFunLike.congr_fun H x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
this : b.symm = b'.symm
⊢ { repr := b : FreeGroupBasis ι G } = { repr := b' }
have rw : b = b'
Tactic: rw [ofRepr.injEq, ← MulEquiv.symm_symm b, ← MulEquiv.symm_symm b', this]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
this : b.symm = b'.symm
rw : b = b'
⊢ { repr := b : FreeGroupBasis ι G } = { repr := b' }
have rw₁ : b.symm.symm = b'
Tactic: rw [ofRepr.injEq, ← MulEquiv.symm_symm b, ← MulEquiv.symm_symm b', this]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
this : b.symm = b'.symm
rw : b = b'
rw₁ : b.symm.symm = b'
⊢ { repr := b : FreeGroupBasis ι G } = { repr := b' }
have rw₂ : b.symm.symm = b'.symm.symm
Tactic: rw [ofRepr.injEq, ← MulEquiv.symm_symm b, ← MulEquiv.symm_symm b', this]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H_1 : Type u_4
inst : Group G
inst_1 : Group H_1
b b' : MulEquiv.{u_3, u_1} G (FreeGroup ι)
hbb' :
  Eq (α := (a : ι) → G)
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b })
    ((fun (b : FreeGroupBasis ι G) (i : ι) ↦ ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i) : G))
      { repr := b' })
H : Eq (α := MonoidHom.{u_1, u_3} (FreeGroup ι) G) (↑b.symm : FreeGroup ι →* G) (↑b'.symm : FreeGroup ι →* G)
this : b.symm = b'.symm
rw : b = b'
rw₁ : b.symm.symm = b'
rw₂ : b.symm.symm = b'.symm.symm
⊢ { repr := b : FreeGroupBasis ι G } = { repr := b' }
have rw₃ : b'.symm.symm = b'.symm.symm
Tactic: rw [ofRepr.injEq, ← MulEquiv.symm_symm b, ← MulEquiv.symm_symm b', this]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
Goal:
ι : Type u_1
G : Type u_3
inst : Group G
b : FreeGroupBasis ι G
i : ι
⊢ (b.repr : (a : G) → FreeGroup ι) ((b : (a : ι) → G) i) = FreeGroup.of i
have change : (b.repr : (a : G) → FreeGroup ι) ((b.repr.symm : (a : FreeGroup ι) → G) (FreeGroup.of i)) = FreeGroup.of i
Tactic: change b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
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
⊢ (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
have 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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
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
⊢ (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
have 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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
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
⊢ 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))
have 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)
Tactic: apply FreeGroup.ext_hom
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
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) :=
  ⋯
⊢ 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)
have 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)
Tactic: apply lift.symm.injective
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.IsFreeGroup (goal)
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) :=
  ⋯
⊢ 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)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
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
have refine_1 : ∀ (g : G), SemidirectProduct.right (N := A → X) (φ := mulAutArrow) ((F' : (a : G) → (A → X) ⋊[mulAutArrow] G) g) = g
Tactic: refine ⟨uncurry F' ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
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'
⊢ ∀ (g : G), SemidirectProduct.right (N := A → X) (φ := mulAutArrow) ((F' : (a : G) → (A → X) ⋊[mulAutArrow] G) g) = g
have refine_1 : MonoidHom.comp SemidirectProduct.rightHom F' = MonoidHom.id G
Tactic: suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id _ by
        exact DFunLike.ext_iff.mp this
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
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'
⊢ MonoidHom.comp SemidirectProduct.rightHom F' = MonoidHom.id G
have 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)
Tactic: apply IsFreeGroup.ext_hom (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
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) ((MonoidHom.comp SemidirectProduct.rightHom F' : (a : G) → G) (IsFreeGroup.of x) : G)
    ((MonoidHom.id G : (a : G) → G) (IsFreeGroup.of x) : G)
have rw : Eq (α := G) ((SemidirectProduct.rightHom : (a : (A → X) ⋊[mulAutArrow] G) → G) (f' x) : G)
  ((MonoidHom.id G : (a : G) → G) (IsFreeGroup.of x) : G)
Tactic: rw [MonoidHom.comp_apply, hF']
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
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'
have a : ∀ (a : IsFreeGroup.Generators G), (curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of a) = f' a
Tactic: apply uF'
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
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
⊢ (curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e) = f' e
have a : ∀ (x : A),
  SemidirectProduct.left (G := G) (φ := mulAutArrow) ((curry E : (a : G) → (A → X) ⋊[mulAutArrow] G) (IsFreeGroup.of e))
      x =
    (f' e).left x
Tactic: ext