awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
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
⊢ 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:
rcases e with ⟨e | e, eT⟩
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
ih : F'.map (homOfPath T p) = 1
e : b ⟶ c
eT : Sum.inl e ∈ T b c
refine_1 : f' e = 1
⊢ 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:
rw [hF']
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
ih : F'.map (homOfPath T p) = 1
e : b ⟶ c
eT : Sum.inl e ∈ T b c
⊢ f' e = 1

Tactic:
dif_pos (Or.inl eT)

Premises used: Set.Mem, setOf, Quiver.wideSubquiverSymmetrify, dif_pos, Or.inl
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
ih : F'.map (homOfPath T p) = 1
e : b ⟶ c
eT : Sum.inl e ∈ T b c
⊢ f' e = 1

Tactic:
exact dif_pos (Or.inl eT)

Premises used: dif_pos, Or.inl
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
ih : F'.map (homOfPath T p) = 1
e : c ⟶ b
eT : Sum.inr e ∈ T b c
refine_1 : f' e = 1
⊢ 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:
rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']

Premises used: inv_eq_one, CategoryTheory.SingleObj.inv_as_inv, CategoryTheory.Functor.map_inv
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
ih : F'.map (homOfPath T p) = 1
e : c ⟶ b
eT : Sum.inr e ∈ T b c
⊢ f' e = 1

Tactic:
dif_pos (Or.inr eT)

Premises used: Set.Mem, setOf, Quiver.wideSubquiverSymmetrify, dif_pos, Or.inr
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
ih : F'.map (homOfPath T p) = 1
e : c ⟶ b
eT : Sum.inr e ∈ T b c
⊢ f' e = 1

Tactic:
exact dif_pos (Or.inr eT)

Premises used: dif_pos, Or.inr
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
refine_1 :
  Eq (α := F'.obj (root' T) ⟶ F'.obj (root (WideSubquiver.toType (Symmetrify (Generators G)) T)))
    (F'.map (homOfPath T Path.nil)) 1
refine_1₁ :
  ∀ {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
⊢ F'.map (homOfPath T p) = 1

Tactic:
induction p with
        | nil => rw [homOfPath, F'.map_id, id_as_one]
        | cons p e ih =>
          rw [homOfPath, F'.map_comp, comp_as_mul, ih, mul_one]
          rcases e with ⟨e | e, eT⟩
          · rw [hF']
            exact dif_pos (Or.inl eT)
          · rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']
            exact dif_pos (Or.inr eT)

Premises used: IsFreeGroupoid.SpanningTree.homOfPath, CategoryTheory.SingleObj.id_as_one, inv_eq_one, CategoryTheory.SingleObj.inv_as_inv, CategoryTheory.SingleObj.comp_as_mul, CategoryTheory.Functor.map_inv, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, mul_one
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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'
E : End (root' T) →* X
hE :
  ∀
    (a :
      (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
              (wideSubquiverSymmetrify T))ᶜ :
        Type u)),
    (E : (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
refine_2 :
  ∀ (x : End (root' T)),
    Eq (α := X) ((E : (a : End (root' T)) → X) x : X) ((Functor.mapEnd (root' T) F' : (a : End (root' T)) → X) x : X)
⊢ E = Functor.mapEnd (root' T) F'

Tactic:
ext x
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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'
E : End (root' T) →* X
hE :
  ∀
    (a :
      (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
              (wideSubquiverSymmetrify T))ᶜ :
        Type u)),
    (E : (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
x : End (root' T)
this : (functorOfMonoidHom T E).map x = F'.map x
⊢ Eq (α := X) ((E : (a : End (root' T)) → X) x : X) ((Functor.mapEnd (root' T) F' : (a : End (root' T)) → X) x : X)

Tactic:
simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root,
            Category.id_comp, Category.comp_id] using this

Premises used: IsFreeGroupoid.SpanningTree.loopOfHom, IsFreeGroupoid.SpanningTree.functorOfMonoidHom, CategoryTheory.IsIso.inv_id, CategoryTheory.Category.comp_id, IsFreeGroupoid.SpanningTree.treeHom_root, CategoryTheory.Category.id_comp
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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'
E : End (root' T) →* X
hE :
  ∀
    (a :
      (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
              (wideSubquiverSymmetrify T))ᶜ :
        Type u)),
    (E : (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
x : End (root' T)
refine_2 : (functorOfMonoidHom T E).map x = F'.map x
⊢ Eq (α := X) ((E : (a : End (root' T)) → X) x : X) ((Functor.mapEnd (root' T) F' : (a : End (root' T)) → X) x : X)

Tactic:
suffices (functorOfMonoidHom T E).map x = F'.map x by
          simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root,
            Category.id_comp, Category.comp_id] using this
-- Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier
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'
E : End (root' T) →* X
hE :
  ∀
    (a :
      (↑((wideSubquiverEquivSetTotal : (a : WideSubquiver (Generators G)) → Set (Quiver.Total (Generators G)))
              (wideSubquiverSymmetrify T))ᶜ :
        Type u)),
    (E : (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
x : End (root' T)
refine_2 : functorOfMonoidHom T E = F'
⊢ (functorOfMonoidHom T E).map x = F'.map x

Tactic:
congr