[GOAL]
G A : Type u
inst✝² : Group G
inst✝¹ : IsFreeGroup G
inst✝ : MulAction G A
⊢ ∀ {X : Type u} [inst : Group X] (f : Labelling (Generators (ActionCategory G A)) X),
    ∃! F,
      ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
        F.map
            ((fun {a b} e =>
                { val := IsFreeGroup.of ↑e,
                  property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
              g) =
          f g
[PROOFSTEP]
intro X _ f
[GOAL]
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
⊢ ∃! F,
    ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
      F.map
          ((fun {a b} e =>
              { val := IsFreeGroup.of ↑e,
                property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
            g) =
        f g
[PROOFSTEP]
let f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e =>
  ⟨fun b => @f ⟨(), _⟩ ⟨(), b⟩ ⟨e, smul_inv_smul _ b⟩, IsFreeGroup.of e⟩
[GOAL]
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
⊢ ∃! F,
    ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
      F.map
          ((fun {a b} e =>
              { val := IsFreeGroup.of ↑e,
                property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
            g) =
        f g
[PROOFSTEP]
rcases IsFreeGroup.unique_lift f' with ⟨F', hF', uF'⟩
[GOAL]
case intro.intro
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ ∃! F,
    ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
      F.map
          ((fun {a b} e =>
              { val := IsFreeGroup.of ↑e,
                property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
            g) =
        f g
[PROOFSTEP]
refine' ⟨uncurry F' _, _, _⟩
[GOAL]
case intro.intro.refine'_1
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ ∀ (g : G), (↑F' g).right = g
[PROOFSTEP]
suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id _ by
  -- Porting note: `MonoidHom.ext_iff` has been deprecated.exact FunLike.ext_iff.mp this
[GOAL]
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
this : MonoidHom.comp SemidirectProduct.rightHom F' = MonoidHom.id G
⊢ ∀ (g : G), (↑F' g).right = g
[PROOFSTEP]
exact FunLike.ext_iff.mp this
[GOAL]
case intro.intro.refine'_1
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ MonoidHom.comp SemidirectProduct.rightHom F' = MonoidHom.id G
[PROOFSTEP]
ext
[GOAL]
case intro.intro.refine'_1.h
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
a✝ : IsFreeGroup.Generators G
⊢ ↑(MonoidHom.comp SemidirectProduct.rightHom F') (IsFreeGroup.of a✝) = ↑(MonoidHom.id G) (IsFreeGroup.of a✝)
[PROOFSTEP]
rw [MonoidHom.comp_apply, hF']
[GOAL]
case intro.intro.refine'_1.h
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
a✝ : IsFreeGroup.Generators G
⊢ ↑SemidirectProduct.rightHom (f' a✝) = ↑(MonoidHom.id G) (IsFreeGroup.of a✝)
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.refine'_2
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ (fun F =>
      ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
        F.map
            ((fun {a b} e =>
                { val := IsFreeGroup.of ↑e,
                  property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
              g) =
          f g)
    (ActionCategory.uncurry F' (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x))
[PROOFSTEP]
rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b⟩ ⟨e, h : IsFreeGroup.of e • a = b⟩
[GOAL]
case intro.intro.refine'_2.mk.unit.mk.unit.mk
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
a : A
b : (actionAsFunctor G A).obj PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • a = b
⊢ (ActionCategory.uncurry F'
          (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)).map
      ((fun {a b} e =>
          { val := IsFreeGroup.of ↑e,
            property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
        { val := e, property := h }) =
    f { val := e, property := h }
[PROOFSTEP]
change (F' (IsFreeGroup.of _)).left _ = _
[GOAL]
case intro.intro.refine'_2.mk.unit.mk.unit.mk
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
a : A
b : (actionAsFunctor G A).obj PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • a = b
⊢ SemidirectProduct.left (↑F' (IsFreeGroup.of ↑{ val := e, property := h }))
      (ActionCategory.back { fst := PUnit.unit, snd := b }) =
    f { val := e, property := h }
[PROOFSTEP]
rw [hF']
[GOAL]
case intro.intro.refine'_2.mk.unit.mk.unit.mk
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
a : A
b : (actionAsFunctor G A).obj PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • a = b
⊢ SemidirectProduct.left (f' ↑{ val := e, property := h }) (ActionCategory.back { fst := PUnit.unit, snd := b }) =
    f { val := e, property := h }
[PROOFSTEP]
cases inv_smul_eq_iff.mpr h.symm
[GOAL]
case intro.intro.refine'_2.mk.unit.mk.unit.mk.refl
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
b : (actionAsFunctor G A).obj PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b
⊢ SemidirectProduct.left (f' ↑{ val := e, property := h }) (ActionCategory.back { fst := PUnit.unit, snd := b }) =
    f { val := e, property := h }
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.refine'_3
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (IsFreeGroup.of a) = f' a) y → y = F'
⊢ ∀ (y : ActionCategory G A ⥤ CategoryTheory.SingleObj X),
    (fun F =>
          ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b),
            F.map
                ((fun {a b} e =>
                    { val := IsFreeGroup.of ↑e,
                      property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
                  g) =
              f g)
        y →
      y =
        ActionCategory.uncurry F'
          (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)
[PROOFSTEP]
intro E hE
[GOAL]
case intro.intro.refine'_3
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
⊢ E = ActionCategory.uncurry F' (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)
[PROOFSTEP]
have : curry E = F' := by
  apply uF'
  intro e
  ext
  · convert hE _ _ _
    rfl
  · rfl
[GOAL]
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
⊢ ActionCategory.curry E = F'
[PROOFSTEP]
apply uF'
[GOAL]
case a
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
⊢ ∀ (a : IsFreeGroup.Generators G), ↑(ActionCategory.curry E) (IsFreeGroup.of a) = f' a
[PROOFSTEP]
intro e
[GOAL]
case a
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
e : IsFreeGroup.Generators G
⊢ ↑(ActionCategory.curry E) (IsFreeGroup.of e) = f' e
[PROOFSTEP]
ext
[GOAL]
case a.left.h
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
e : IsFreeGroup.Generators G
x✝ : A
⊢ SemidirectProduct.left (↑(ActionCategory.curry E) (IsFreeGroup.of e)) x✝ = SemidirectProduct.left (f' e) x✝
[PROOFSTEP]
convert hE _ _ _
[GOAL]
case h.e'_2.h
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
e : IsFreeGroup.Generators G
x✝ : A
e_1✝ :
  X =
    (E.obj
        (let_fun this := { fst := (), snd := (IsFreeGroup.of e)⁻¹ • x✝ };
        this) ⟶
      E.obj { fst := (), snd := x✝ })
⊢ SemidirectProduct.left (↑(ActionCategory.curry E) (IsFreeGroup.of e)) x✝ =
    E.map
      ((fun {a b} e =>
          { val := IsFreeGroup.of ↑e,
            property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
        { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • x✝ = x✝) })
[PROOFSTEP]
rfl
[GOAL]
case a.right
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
e : IsFreeGroup.Generators G
⊢ (↑(ActionCategory.curry E) (IsFreeGroup.of e)).right = (f' e).right
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.refine'_3
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
this : ActionCategory.curry E = F'
⊢ E = ActionCategory.uncurry F' (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)
[PROOFSTEP]
apply Functor.hext
[GOAL]
case intro.intro.refine'_3.h_obj
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
this : ActionCategory.curry E = F'
⊢ ∀ (X_1 : ActionCategory G A),
    E.obj X_1 =
      (ActionCategory.uncurry F'
            (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)).obj
        X_1
[PROOFSTEP]
intro
[GOAL]
case intro.intro.refine'_3.h_obj
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
this : ActionCategory.curry E = F'
X✝ : ActionCategory G A
⊢ E.obj X✝ =
    (ActionCategory.uncurry F'
          (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)).obj
      X✝
[PROOFSTEP]
apply Unit.ext
[GOAL]
case intro.intro.refine'_3.h_map
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
this : ActionCategory.curry E = F'
⊢ ∀ (X_1 Y : ActionCategory G A) (f : X_1 ⟶ Y),
    HEq (E.map f)
      ((ActionCategory.uncurry F'
            (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)).map
        f)
[PROOFSTEP]
refine' ActionCategory.cases _
[GOAL]
case intro.intro.refine'_3.h_map
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
this : ActionCategory.curry E = F'
⊢ ∀ (t : A) (g : G),
    HEq (E.map (homOfPair t g))
      ((ActionCategory.uncurry F'
            (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)).map
        (homOfPair t g))
[PROOFSTEP]
intros
[GOAL]
case intro.intro.refine'_3.h_map
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
this : ActionCategory.curry E = F'
t✝ : A
g✝ : G
⊢ HEq (E.map (homOfPair t✝ g✝))
    ((ActionCategory.uncurry F'
          (_ : ∀ (x : G), ↑(MonoidHom.comp SemidirectProduct.rightHom F') x = ↑(MonoidHom.id G) x)).map
      (homOfPair t✝ g✝))
[PROOFSTEP]
simp only [← this, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
[GOAL]
case intro.intro.refine'_3.h_map
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G :=
  fun e =>
    { left := fun b => f { val := e, property := (_ : IsFreeGroup.of e • (IsFreeGroup.of e)⁻¹ • b = b) },
      right := IsFreeGroup.of e }
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), ↑F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F => ∀ (a : IsFreeGroup.Generators G), ↑F (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
        ((fun {a b} e =>
            { val := IsFreeGroup.of ↑e,
              property := (_ : IsFreeGroup.of ↑e • ActionCategory.back a = ActionCategory.back b) })
          g) =
      f g
this : ActionCategory.curry E = F'
t✝ : A
g✝ : G
⊢ HEq (E.map (homOfPair t✝ g✝)) (E.map (homOfPair t✝ g✝))
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a : G
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
⊢ treeHom T a = homOfPath T p
[PROOFSTEP]
rw [treeHom, Unique.default_eq]
[GOAL]
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ loopOfHom T (of e) = 𝟙 (IsFreeGroupoid.SpanningTree.root' T)
[PROOFSTEP]
rw [loopOfHom, ← Category.assoc, IsIso.comp_inv_eq, Category.id_comp]
[GOAL]
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b
[PROOFSTEP]
cases' H with H H
[GOAL]
case inl
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T a b (Sum.inl e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b
[PROOFSTEP]
rw [treeHom_eq T (Path.cons default ⟨Sum.inl e, H⟩), homOfPath]
[GOAL]
case inl
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T a b (Sum.inl e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    homOfPath T default ≫ Sum.recOn (↑{ val := Sum.inl e, property := H }) (fun e => of e) fun e => inv (of e)
[PROOFSTEP]
rfl
[GOAL]
case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T b a (Sum.inr e)
⊢ treeHom T
        (let_fun this := a;
        this) ≫
      of e =
    treeHom T b
[PROOFSTEP]
rw [treeHom_eq T (Path.cons default ⟨Sum.inr e, H⟩), homOfPath]
[GOAL]
case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : T b a (Sum.inr e)
⊢ (homOfPath T default ≫ Sum.recOn (↑{ val := Sum.inr e, property := H }) (fun e => of e) fun e => inv (of e)) ≫ of e =
    treeHom T b
[PROOFSTEP]
simp only [IsIso.inv_hom_id, Category.comp_id, Category.assoc, treeHom]
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.65107
inst✝ : Monoid X
f : End (IsFreeGroupoid.SpanningTree.root' T) →* X
⊢ ∀ (X_1 : G),
    { obj := fun x => (), map := fun {X_2 Y} p => ↑f (loopOfHom T p) }.map (𝟙 X_1) =
      𝟙 ({ obj := fun x => (), map := fun {X_2 Y} p => ↑f (loopOfHom T p) }.obj X_1)
[PROOFSTEP]
intro a
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.65107
inst✝ : Monoid X
f : End (IsFreeGroupoid.SpanningTree.root' T) →* X
a : G
⊢ { obj := fun x => (), map := fun {X_1 Y} p => ↑f (loopOfHom T p) }.map (𝟙 a) =
    𝟙 ({ obj := fun x => (), map := fun {X_1 Y} p => ↑f (loopOfHom T p) }.obj a)
[PROOFSTEP]
dsimp only [loopOfHom]
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.65107
inst✝ : Monoid X
f : End (IsFreeGroupoid.SpanningTree.root' T) →* X
a : G
⊢ ↑f (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) = 𝟙 ()
[PROOFSTEP]
rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.65107
inst✝ : Monoid X
f : End (IsFreeGroupoid.SpanningTree.root' T) →* X
⊢ ∀ {X_1 Y Z : G} (f_1 : X_1 ⟶ Y) (g : Y ⟶ Z),
    { obj := fun x => (), map := fun {X_2 Y} p => ↑f (loopOfHom T p) }.map (f_1 ≫ g) =
      { obj := fun x => (), map := fun {X_2 Y} p => ↑f (loopOfHom T p) }.map f_1 ≫
        { obj := fun x => (), map := fun {X_2 Y} p => ↑f (loopOfHom T p) }.map g
[PROOFSTEP]
intros
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.65107
inst✝ : Monoid X
f : End (IsFreeGroupoid.SpanningTree.root' T) →* X
X✝ Y✝ Z✝ : G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun x => (), map := fun {X_1 Y} p => ↑f (loopOfHom T p) }.map (f✝ ≫ g✝) =
    { obj := fun x => (), map := fun {X_1 Y} p => ↑f (loopOfHom T p) }.map f✝ ≫
      { obj := fun x => (), map := fun {X_1 Y} p => ↑f (loopOfHom T p) }.map g✝
[PROOFSTEP]
rw [comp_as_mul, ← f.map_mul]
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.65107
inst✝ : Monoid X
f : End (IsFreeGroupoid.SpanningTree.root' T) →* X
X✝ Y✝ Z✝ : G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun x => (), map := fun {X_1 Y} p => ↑f (loopOfHom T p) }.map (f✝ ≫ g✝) =
    ↑f (loopOfHom T g✝ * loopOfHom T f✝)
[PROOFSTEP]
simp only [IsIso.inv_hom_id_assoc, loopOfHom, End.mul_def, Category.assoc]
[GOAL]
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
⊢ ∀ {H : Type u} [inst : Group H] (f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → H),
    ∃! F,
      ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ),
        ↑F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
[PROOFSTEP]
intro X _ f
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
⊢ ∃! F,
    ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ),
      ↑F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
[PROOFSTEP]
let f' : Labelling (Generators G) X := fun a b e =>
  if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨⟨a, b, e⟩, h⟩
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := h }
⊢ ∃! F,
    ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ),
      ↑F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
[PROOFSTEP]
rcases unique_lift f' with ⟨F', hF', uF'⟩
[GOAL]
case intro.intro
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
⊢ ∃! F,
    ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ),
      ↑F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
[PROOFSTEP]
refine' ⟨F'.mapEnd _, _, _⟩
[GOAL]
case intro.intro.refine'_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
⊢ (fun F =>
      ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ),
        ↑F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a)
    (Functor.mapEnd (IsFreeGroupoid.SpanningTree.root' T) F')
[PROOFSTEP]
suffices ∀ {x y} (q : x ⟶ y), F'.map (loopOfHom T q) = (F'.map q : X)
  by
  rintro ⟨⟨a, b, e⟩, h⟩
  erw [Functor.mapEnd_apply, this, hF']
  exact dif_neg h
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
this : ∀ {x y : G} (q : x ⟶ y), F'.map (loopOfHom T q) = F'.map q
⊢ (fun F =>
      ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ),
        ↑F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a)
    (Functor.mapEnd (IsFreeGroupoid.SpanningTree.root' T) F')
[PROOFSTEP]
rintro ⟨⟨a, b, e⟩, h⟩
[GOAL]
case mk.mk
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
this : ∀ {x y : G} (q : x ⟶ y), F'.map (loopOfHom T q) = F'.map q
a b : Generators G
e : a ⟶ b
h : { left := a, right := b, hom := e } ∈ (↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ
⊢ ↑(Functor.mapEnd (IsFreeGroupoid.SpanningTree.root' T) F')
      ((fun e => loopOfHom T (of (↑e).hom)) { val := { left := a, right := b, hom := e }, property := h }) =
    f { val := { left := a, right := b, hom := e }, property := h }
[PROOFSTEP]
erw [Functor.mapEnd_apply, this, hF']
[GOAL]
case mk.mk
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
this : ∀ {x y : G} (q : x ⟶ y), F'.map (loopOfHom T q) = F'.map q
a b : Generators G
e : a ⟶ b
h : { left := a, right := b, hom := e } ∈ (↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ
⊢ f' (↑{ val := { left := a, right := b, hom := e }, property := h }).hom =
    f { val := { left := a, right := b, hom := e }, property := h }
[PROOFSTEP]
exact dif_neg h
[GOAL]
case intro.intro.refine'_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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
[PROOFSTEP]
intros x y q
[GOAL]
case intro.intro.refine'_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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
[PROOFSTEP]
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]
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
this :
  ∀ {a : WideSubquiver.toType (Symmetrify (Generators G)) T}
    (p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a), F'.map (homOfPath T p) = 1
⊢ F'.map (loopOfHom T q) = F'.map q
[PROOFSTEP]
simp only [this, treeHom, comp_as_mul, inv_as_inv, loopOfHom, inv_one, mul_one, one_mul, Functor.map_inv,
  Functor.map_comp]
[GOAL]
case intro.intro.refine'_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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), F'.map (homOfPath T p) = 1
[PROOFSTEP]
intro a p
[GOAL]
case intro.intro.refine'_1
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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
⊢ F'.map (homOfPath T p) = 1
[PROOFSTEP]
induction' p with b c p e ih
[GOAL]
case intro.intro.refine'_1.nil
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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
⊢ F'.map (homOfPath T Path.nil) = 1
[PROOFSTEP]
rw [homOfPath, F'.map_id, id_as_one]
[GOAL]
case intro.intro.refine'_1.cons
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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 (Path.cons p e)) = 1
[PROOFSTEP]
rw [homOfPath, F'.map_comp, comp_as_mul, ih, mul_one]
[GOAL]
case intro.intro.refine'_1.cons
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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 (Sum.recOn (↑e) (fun e => of e) fun e => inv (of e)) = 1
[PROOFSTEP]
rcases e with ⟨e | e, eT⟩
[GOAL]
case intro.intro.refine'_1.cons.mk.inl
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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'.map (Sum.recOn (↑{ val := Sum.inl e, property := eT }) (fun e => of e) fun e => inv (of e)) = 1
[PROOFSTEP]
rw [hF']
[GOAL]
case intro.intro.refine'_1.cons.mk.inl
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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
[PROOFSTEP]
exact dif_pos (Or.inl eT)
[GOAL]
case intro.intro.refine'_1.cons.mk.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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'.map (Sum.recOn (↑{ val := Sum.inr e, property := eT }) (fun e => of e) fun e => inv (of e)) = 1
[PROOFSTEP]
rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']
[GOAL]
case intro.intro.refine'_1.cons.mk.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (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
[PROOFSTEP]
exact dif_pos (Or.inr eT)
[GOAL]
case intro.intro.refine'_2
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
⊢ ∀ (y : End (IsFreeGroupoid.SpanningTree.root' T) →* X),
    (fun F =>
          ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ),
            ↑F ((fun e => loopOfHom T (of (↑e).hom)) a) = f a)
        y →
      y = Functor.mapEnd (IsFreeGroupoid.SpanningTree.root' T) F'
[PROOFSTEP]
intro E hE
[GOAL]
case intro.intro.refine'_2
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
⊢ E = Functor.mapEnd (IsFreeGroupoid.SpanningTree.root' T) F'
[PROOFSTEP]
ext x
[GOAL]
case intro.intro.refine'_2.h
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
⊢ ↑E x = ↑(Functor.mapEnd (IsFreeGroupoid.SpanningTree.root' T) F') x
[PROOFSTEP]
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
[GOAL]
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
this : (functorOfMonoidHom T E).map x = F'.map x
⊢ ↑E x = ↑(Functor.mapEnd (IsFreeGroupoid.SpanningTree.root' T) F') x
[PROOFSTEP]
simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root, Category.id_comp, Category.comp_id] using this
[GOAL]
case intro.intro.refine'_2.h
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
⊢ (functorOfMonoidHom T E).map x = F'.map x
[PROOFSTEP]
congr
[GOAL]
case intro.intro.refine'_2.h.h.e_5.h.e_self
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
⊢ functorOfMonoidHom T E = F'
[PROOFSTEP]
apply uF'
[GOAL]
case intro.intro.refine'_2.h.h.e_5.h.e_self.a
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
⊢ ∀ (a b : Generators G) (g : a ⟶ b), (functorOfMonoidHom T E).map (of g) = f' g
[PROOFSTEP]
intro a b e
[GOAL]
case intro.intro.refine'_2.h.h.e_5.h.e_self.a
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
a b : Generators G
e : a ⟶ b
⊢ (functorOfMonoidHom T E).map (of e) = f' e
[PROOFSTEP]
change E (loopOfHom T _) = dite _ _ _
[GOAL]
case intro.intro.refine'_2.h.h.e_5.h.e_self.a
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
a b : Generators G
e : a ⟶ b
⊢ ↑E (loopOfHom T (of e)) =
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := h }
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
a b : Generators G
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
⊢ ↑E (loopOfHom T (of e)) = 1
[PROOFSTEP]
rw [loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
[GOAL]
case neg
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e =>
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f { val := { left := a, right := b, hom := e }, property := 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 => ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (IsFreeGroupoid.SpanningTree.root' T) →* X
hE :
  ∀ (a : ↑(↑wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), ↑E ((fun e => loopOfHom T (of (↑e).hom)) a) = f a
x : End (IsFreeGroupoid.SpanningTree.root' T)
a b : Generators G
e : a ⟶ b
h : ¬e ∈ wideSubquiverSymmetrify T a b
⊢ ↑E (loopOfHom T (of e)) = f { val := { left := a, right := b, hom := e }, property := h }
[PROOFSTEP]
exact hE ⟨⟨a, b, e⟩, h⟩
[GOAL]
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
⊢ Nonempty (a ⟶ b) → Nonempty (Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))
[PROOFSTEP]
rintro ⟨p⟩
[GOAL]
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ Nonempty (Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))
[PROOFSTEP]
rw [← @WeaklyConnectedComponent.eq (Generators G), eq_comm, ← FreeGroup.of_injective.eq_iff, ← mul_inv_eq_one]
[GOAL]
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1
[PROOFSTEP]
let X := FreeGroup (WeaklyConnectedComponent <| Generators G)
[GOAL]
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1
[PROOFSTEP]
let f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
[GOAL]
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1
[PROOFSTEP]
let F : G ⥤ CategoryTheory.SingleObj.{u} (X : Type u) := SingleObj.differenceFunctor f
[GOAL]
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) *
      (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ =
    1
[PROOFSTEP]
change (F.map p) = ((@CategoryTheory.Functor.const G _ _ (SingleObj.category X)).obj ()).map p
[GOAL]
case intro
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ F.map p = ((Functor.const G).obj ()).map p
[PROOFSTEP]
congr
[GOAL]
case intro.h.e_5.h.e_self
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ F = (Functor.const G).obj ()
[PROOFSTEP]
ext
[GOAL]
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ F.map (of e✝) = ((Functor.const G).obj ()).map (of e✝)
[PROOFSTEP]
rw [Functor.const_obj_map, id_as_one, differenceFunctor_map, @mul_inv_eq_one _ _ (f _)]
[GOAL]
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ f b✝ =
    f
      (let_fun this := a✝;
      this)
[PROOFSTEP]
apply congr_arg FreeGroup.of
[GOAL]
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ WeaklyConnectedComponent.mk b✝ =
    WeaklyConnectedComponent.mk
      (let_fun this := a✝;
      this)
[PROOFSTEP]
apply (WeaklyConnectedComponent.eq _ _).mpr
[GOAL]
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ Nonempty
    (Path b✝
      (let_fun this := a✝;
      this))
[PROOFSTEP]
exact ⟨Hom.toPath (Sum.inr (by assumption))⟩
[GOAL]
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ (let_fun this := a✝;
    this) ⟶
    b✝
[PROOFSTEP]
assumption