-- 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'
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)
a b : Generators G
e : a ⟶ b
pos :
  ∀ (h : e ∈ wideSubquiverSymmetrify T a b),
    Eq (α := X) ((E : (a : End (root' T)) → X) (loopOfHom T (of e)) : X) (1 : X)
⊢ Eq (α := X) ((E : (a : End (root' T)) → X) (loopOfHom T (of e)) : X)
    (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) :
      X)
have neg : ∀ (h : e ∉ wideSubquiverSymmetrify T a b),
  (E : (a : End (root' T)) → X) (loopOfHom T (of e)) =
    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 : Quiver.Total (Generators G) } h)
Tactic: split_ifs with h