awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u_1
inst_3 : Monoid X
f : MonoidHom.{u, u_1} (End (root' T)) X
a : G
rw : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ inv (treeHom T a)) : X) (𝟙 () : () ⟶ ())
rw₁ : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (𝟙 (root' T)) : X) (𝟙 () : () ⟶ ())
⊢ Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) : X)
    (𝟙 () : () ⟶ ())
have rw₂ : Eq (α := () ⟶ ()) ((f : (a : End (root' T)) → X) 1 : X) (𝟙 () : () ⟶ ())
Tactic: rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u_1
inst_3 : Monoid X
f : MonoidHom.{u, u_1} (End (root' T)) X
a : G
rw : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ inv (treeHom T a)) : X) (𝟙 () : () ⟶ ())
rw₁ : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (𝟙 (root' T)) : X) (𝟙 () : () ⟶ ())
rw₂ : Eq (α := () ⟶ ()) ((f : (a : End (root' T)) → X) 1 : X) (𝟙 () : () ⟶ ())
⊢ Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) : X)
    (𝟙 () : () ⟶ ())
have rw₃ : Eq.{u_1 + 1} (α := () ⟶ ()) (1 : X) (𝟙 () : () ⟶ ())
Tactic: rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u_1
inst_3 : Monoid X
f : MonoidHom.{u, u_1} (End (root' T)) X
a : G
rw : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ inv (treeHom T a)) : X) (𝟙 () : () ⟶ ())
rw₁ : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (𝟙 (root' T)) : X) (𝟙 () : () ⟶ ())
rw₂ : Eq (α := () ⟶ ()) ((f : (a : End (root' T)) → X) 1 : X) (𝟙 () : () ⟶ ())
rw₃ : Eq.{u_1 + 1} (α := () ⟶ ()) (1 : X) (𝟙 () : () ⟶ ())
⊢ Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) : X)
    (𝟙 () : () ⟶ ())
have rw₄ : Eq.{u_1 + 1} (α := () ⟶ ()) 1 1
Tactic: rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u_1
inst_3 : Monoid X
f : MonoidHom.{u, u_1} (End (root' T)) X
X_1 Y Z : G
f_1 : X_1 ⟶ Y
g : Y ⟶ Z
⊢ Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (loopOfHom T (f_1 ≫ g)) : X)
    (CategoryStruct.comp (Y := ()) ((f : (a : End (root' T)) → X) (loopOfHom T f_1))
        ((f : (a : End (root' T)) → X) (loopOfHom T g)) :
      () ⟶ ())
have rw : Eq.{u_1 + 1} (α := () ⟶ ()) ((f : (a : End (root' T)) → X) (loopOfHom T (f_1 ≫ g)) : X)
  ((f : (a : End (root' T)) → X) (HMul.hMul (α := End (root' T)) (loopOfHom T g) (loopOfHom T f_1)) : X)
Tactic: rw [comp_as_mul, ← f.map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
⊢ ∃! F : End (root' T) →* X,
    ∀
      (a :
        (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                (wideSubquiverSymmetrify T))ᶜ :
          Type u)),
      (F : (a : End (root' T)) → X)
          ((fun
                (e :
                  (↑((wideSubquiverEquivSetTotal :
                            (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                          (wideSubquiverSymmetrify T))ᶜ :
                    Type u)) ↦
              (loopOfHom T (of (↑e : Quiver.Total (Generators G)).hom) : End (root' T)))
            a) =
        f a
have rcases : ∀ (F' : G ⥤ CategoryTheory.SingleObj X) (hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g)
  (uF' :
    ∀ (y : G ⥤ CategoryTheory.SingleObj X),
      (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'),
  ∃! F : End (root' T) →* X,
    ∀
      (a :
        (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                (wideSubquiverSymmetrify T))ᶜ :
          Type u)),
      (F : (a : End (root' T)) → X)
          ((fun
                (e :
                  (↑((wideSubquiverEquivSetTotal :
                            (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                          (wideSubquiverSymmetrify T))ᶜ :
                    Type u)) ↦
              (loopOfHom T (of (↑e : Quiver.Total (Generators G)).hom) : End (root' T)))
            a) =
        f a
Tactic: rcases unique_lift f' with ⟨F', hF', uF'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
⊢ ∃! F : End (root' T) →* X,
    ∀
      (a :
        (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                (wideSubquiverSymmetrify T))ᶜ :
          Type u)),
      (F : (a : End (root' T)) → X)
          ((fun
                (e :
                  (↑((wideSubquiverEquivSetTotal :
                            (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                          (wideSubquiverSymmetrify T))ᶜ :
                    Type u)) ↦
              (loopOfHom T (of (↑e : Quiver.Total (Generators G)).hom) : End (root' T)))
            a) =
        f a
have refine_1 : (fun (F : End (root' T) →* X) ↦
    ∀
      (a :
        (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                (wideSubquiverSymmetrify T))ᶜ :
          Type u)),
      (F : (a : End (root' T)) → X)
          ((fun
                (e :
                  (↑((wideSubquiverEquivSetTotal :
                            (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                          (wideSubquiverSymmetrify T))ᶜ :
                    Type u)) ↦
              (loopOfHom T (of (↑e : Quiver.Total (Generators G)).hom) : End (root' T)))
            a) =
        f a)
  (Functor.mapEnd (root' T) F')
Tactic: refine ⟨F'.mapEnd _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
⊢ (fun (F : End (root' T) →* X) ↦
      ∀
        (a :
          (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
            Type u)),
        (F : (a : End (root' T)) → X)
            ((fun
                  (e :
                    (↑((wideSubquiverEquivSetTotal :
                              (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                            (wideSubquiverSymmetrify T))ᶜ :
                      Type u)) ↦
                (loopOfHom T (of (↑e : Quiver.Total (Generators G)).hom) : End (root' T)))
              a) =
          f a)
    (Functor.mapEnd (root' T) F')
have refine_1 : ∀ {x y : G} (q : x ⟶ y), F'.map (loopOfHom T q) = F'.map q
Tactic: suffices ∀ {x y} (q : x ⟶ y), F'.map (loopOfHom T q) = (F'.map q : X) by
          rintro ⟨⟨a, b, e⟩, h⟩
          simp only [Functor.mapEnd, DFunLike.coe, this, hF']
          exact dif_neg h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
⊢ F'.map (loopOfHom T q) = F'.map q
have refine_1 : ∀ {a : WideSubquiver.toType (Symmetrify (Generators G)) T}
  (p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a), F'.map (homOfPath T p) = 1
Tactic: suffices ∀ {a} (p : Path (root T) a), F'.map (homOfPath T p) = 1 by
          simp only [this, treeHom, comp_as_mul, inv_as_inv, loopOfHom, inv_one, mul_one,
            one_mul, Functor.map_inv, Functor.map_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a : WideSubquiver.toType (Symmetrify (Generators G)) T
⊢ Eq (α := F'.obj (root' T) ⟶ F'.obj (root (WideSubquiver.toType (Symmetrify (Generators G)) T)))
    (F'.map (homOfPath T Path.nil)) 1
have refine_1 : F'.map (𝟙 (root' T)) = 1
Tactic: rw [homOfPath, F'.map_id, id_as_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a : WideSubquiver.toType (Symmetrify (Generators G)) T
refine_1 : F'.map (𝟙 (root' T)) = 1
⊢ Eq (α := F'.obj (root' T) ⟶ F'.obj (root (WideSubquiver.toType (Symmetrify (Generators G)) T)))
    (F'.map (homOfPath T Path.nil)) 1
have refine_1₁ : Eq.{u + 1} (α := F'.obj (root' T) ⟶ F'.obj (root (WideSubquiver.toType (Symmetrify (Generators G)) T)))
  (𝟙 (F'.obj (root' T))) 1
Tactic: rw [homOfPath, F'.map_id, id_as_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a : WideSubquiver.toType (Symmetrify (Generators G)) T
refine_1 : F'.map (𝟙 (root' T)) = 1
refine_1₁ :
  Eq.{u + 1} (α := F'.obj (root' T) ⟶ F'.obj (root (WideSubquiver.toType (Symmetrify (Generators G)) T)))
    (𝟙 (F'.obj (root' T))) 1
⊢ Eq (α := F'.obj (root' T) ⟶ F'.obj (root (WideSubquiver.toType (Symmetrify (Generators G)) T)))
    (F'.map (homOfPath T Path.nil)) 1
have refine_1₂ : Eq.{u + 1} (α := F'.obj (root' T) ⟶ F'.obj (root (WideSubquiver.toType (Symmetrify (Generators G)) T))) 1 1
Tactic: rw [homOfPath, F'.map_id, id_as_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b c : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b
e : b ⟶ c
ih : F'.map (homOfPath T p) = 1
⊢ F'.map (homOfPath T (p.cons e)) = 1
have refine_1 : Eq (α := F'.obj (root' T) ⟶ F'.obj c)
  (F'.map
    (Sum.recOn (motive := fun (x : b ⟶ c) ↦ b ⟶ c) (↑e : b ⟶ c) (fun (e : b ⟶ c) ↦ of e) fun (e : c ⟶ b) ↦ inv (of e)))
  1
Tactic: rw [homOfPath, F'.map_comp, comp_as_mul, ih, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b c : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b
e : b ⟶ c
ih : F'.map (homOfPath T p) = 1
⊢ Eq (α := F'.obj (root' T) ⟶ F'.obj c)
    (F'.map
      (Sum.recOn (motive := fun (x : b ⟶ c) ↦ b ⟶ c) (↑e : b ⟶ c) (fun (e : b ⟶ c) ↦ of e) fun (e : c ⟶ b) ↦
        inv (of e)))
    1
have refine_1 : ∀ (e : b ⟶ c) (eT : Sum.inl e ∈ T b c),
  Eq (α := F'.obj (root' T) ⟶ F'.obj c)
    (F'.map
      (Sum.recOn (motive := fun (x : b ⟶ c) ↦ b ⟶ c)
        (↑(Subtype.mk (p := fun (f : b ⟶ c) ↦ f ∈ T b c) (Sum.inl e) eT) : b ⟶ c) (fun (e : b ⟶ c) ↦ of e)
        fun (e : c ⟶ b) ↦ inv (of e)))
    1
Tactic: rcases e with ⟨e | e, eT⟩
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.NielsenSchreier (goal)
Goal:
G : Type u
inst : Groupoid G
inst_1 : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst_2 : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst_3 : Group X
f :
  (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
            (wideSubquiverSymmetrify T))ᶜ :
      Type u) →
    X
f' : Labelling (Generators G) X :=
  fun (a b : Generators G) (e : a ⟶ b) ↦
    if h : e ∈ wideSubquiverSymmetrify T a b then 1
    else
      f
        (Subtype.mk (p := fun (x : Quiver.Total (Generators G)) ↦
          Membership.mem (γ := Set (Quiver.Total (Generators G)))
            (((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
                  (wideSubquiverSymmetrify T))ᶜ :
              Set (Quiver.Total (Generators G)))
            x)
          { left := a, right := b, hom := e } h)
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X),
    (fun (F : G ⥤ CategoryTheory.SingleObj X) ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b c : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b
e : b ⟶ c
ih : F'.map (homOfPath T p) = 1
refine_1 :
  ∀ (e : b ⟶ c) (eT : Sum.inl e ∈ T b c),
    Eq (α := F'.obj (root' T) ⟶ F'.obj c)
      (F'.map
        (Sum.recOn (motive := fun (x : b ⟶ c) ↦ b ⟶ c)
          (↑(Subtype.mk (p := fun (f : b ⟶ c) ↦ f ∈ T b c) (Sum.inl e) eT) : b ⟶ c) (fun (e : b ⟶ c) ↦ of e)
          fun (e : c ⟶ b) ↦ inv (of e)))
      1
⊢ Eq (α := F'.obj (root' T) ⟶ F'.obj c)
    (F'.map
      (Sum.recOn (motive := fun (x : b ⟶ c) ↦ b ⟶ c) (↑e : b ⟶ c) (fun (e : b ⟶ c) ↦ of e) fun (e : c ⟶ b) ↦
        inv (of e)))
    1
have refine_1₁ : ∀ (e : c ⟶ b) (eT : Sum.inr e ∈ T b c),
  Eq (α := F'.obj (root' T) ⟶ F'.obj c)
    (F'.map
      (Sum.recOn (motive := fun (x : b ⟶ c) ↦ b ⟶ c)
        (↑(Subtype.mk (p := fun (f : b ⟶ c) ↦ f ∈ T b c) (Sum.inr e) eT) : b ⟶ c) (fun (e : b ⟶ c) ↦ of e)
        fun (e : c ⟶ b) ↦ inv (of e)))
    1
Tactic: rcases e with ⟨e | e, eT⟩
Cleared hypotheses: e