[GOAL]
V✝ : Type u
inst✝² : Quiver V✝
V : Type ?u.991
inst✝¹ : Quiver V
inst✝ : Nonempty V
⊢ Nonempty (FreeGroupoid V)
[PROOFSTEP]
inhabit V
[GOAL]
V✝ : Type u
inst✝² : Quiver V✝
V : Type ?u.991
inst✝¹ : Quiver V
inst✝ : Nonempty V
inhabited_h : Inhabited V
⊢ Nonempty (FreeGroupoid V)
[PROOFSTEP]
exact ⟨⟨@default V _⟩⟩
[GOAL]
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p q : X ⟶ Y
⊢ Quotient.CompClosure redStep p q → Quotient.CompClosure redStep (Quiver.Path.reverse p) (Quiver.Path.reverse q)
[PROOFSTEP]
rintro ⟨XW, pp, qq, WY, _, Z, f⟩
[GOAL]
case intro.step
V : Type u
inst✝ : Quiver V
X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)
X✝ Z : Quiver.Symmetrify V
f : X✝ ⟶ Z
XW : X✝¹ ⟶ Paths.of.obj X✝
WY : Paths.of.obj X✝ ⟶ Y✝
⊢ Quotient.CompClosure redStep (Quiver.Path.reverse (XW ≫ 𝟙 (Paths.of.obj X✝) ≫ WY))
    (Quiver.Path.reverse (XW ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ WY))
[PROOFSTEP]
have :
  Quotient.CompClosure redStep (WY.reverse ≫ 𝟙 _ ≫ XW.reverse)
    (WY.reverse ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ XW.reverse) :=
  by
  constructor
  constructor
[GOAL]
V : Type u
inst✝ : Quiver V
X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)
X✝ Z : Quiver.Symmetrify V
f : X✝ ⟶ Z
XW : X✝¹ ⟶ Paths.of.obj X✝
WY : Paths.of.obj X✝ ⟶ Y✝
⊢ Quotient.CompClosure redStep (Quiver.Path.reverse WY ≫ 𝟙 (Paths.of.obj X✝) ≫ Quiver.Path.reverse XW)
    (Quiver.Path.reverse WY ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse XW)
[PROOFSTEP]
constructor
[GOAL]
case h
V : Type u
inst✝ : Quiver V
X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)
X✝ Z : Quiver.Symmetrify V
f : X✝ ⟶ Z
XW : X✝¹ ⟶ Paths.of.obj X✝
WY : Paths.of.obj X✝ ⟶ Y✝
⊢ redStep (𝟙 (Paths.of.obj X✝)) (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f))
[PROOFSTEP]
constructor
[GOAL]
case intro.step
V : Type u
inst✝ : Quiver V
X✝¹ Y✝ X Y : Paths (Quiver.Symmetrify V)
X✝ Z : Quiver.Symmetrify V
f : X✝ ⟶ Z
XW : X✝¹ ⟶ Paths.of.obj X✝
WY : Paths.of.obj X✝ ⟶ Y✝
this :
  Quotient.CompClosure redStep (Quiver.Path.reverse WY ≫ 𝟙 (Paths.of.obj X✝) ≫ Quiver.Path.reverse XW)
    (Quiver.Path.reverse WY ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse XW)
⊢ Quotient.CompClosure redStep (Quiver.Path.reverse (XW ≫ 𝟙 (Paths.of.obj X✝) ≫ WY))
    (Quiver.Path.reverse (XW ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ WY))
[PROOFSTEP]
simpa only [CategoryStruct.comp, CategoryStruct.id, Quiver.Path.reverse, Quiver.Path.nil_comp, Quiver.Path.reverse_comp,
  Quiver.reverse_reverse, Quiver.Path.reverse_toPath, Quiver.Path.comp_assoc] using this
[GOAL]
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (p ≫ Quiver.Path.reverse p) = Quot.mk (Quotient.CompClosure redStep) (𝟙 X)
[PROOFSTEP]
apply Quot.EqvGen_sound
[GOAL]
case H
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ EqvGen (Quotient.CompClosure redStep) (p ≫ Quiver.Path.reverse p) (𝟙 X)
[PROOFSTEP]
induction' p with a b q f ih
[GOAL]
case H.nil
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.nil ≫ Quiver.Path.reverse Quiver.Path.nil) (𝟙 X)
[PROOFSTEP]
apply EqvGen.refl
[GOAL]
case H.cons
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.cons q f ≫ Quiver.Path.reverse (Quiver.Path.cons q f)) (𝟙 X)
[PROOFSTEP]
simp only [Quiver.Path.reverse]
[GOAL]
case H.cons
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q)) (𝟙 X)
[PROOFSTEP]
fapply EqvGen.trans
[GOAL]
case H.cons.y
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ X ⟶ X
[PROOFSTEP]
exact q ≫ Quiver.Path.reverse q
[GOAL]
case H.cons.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
    (q ≫ Quiver.Path.reverse q)
[PROOFSTEP]
apply EqvGen.symm
[GOAL]
case H.cons.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
[PROOFSTEP]
apply EqvGen.rel
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
[PROOFSTEP]
have :
  Quotient.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q) :=
  by
  apply Quotient.CompClosure.intro
  apply redStep.step
[GOAL]
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
[PROOFSTEP]
apply Quotient.CompClosure.intro
[GOAL]
case h
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ redStep (𝟙 a) (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f))
[PROOFSTEP]
apply redStep.step
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
[PROOFSTEP]
simp only [Category.assoc, Category.id_comp] at this ⊢
  -- Porting note : `simp` cannot see how `Quiver.Path.comp_assoc` is relevant, so change to
        -- category notation
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (q ≫ Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
[PROOFSTEP]
change
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ (Quiver.Hom.toPath (Quiver.reverse f)) ≫ (Quiver.Path.reverse q))
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (q ≫ Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
[PROOFSTEP]
simp only [← Category.assoc] at this ⊢
[GOAL]
case H.cons.a.a.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (((q ≫ Quiver.Hom.toPath f) ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    ((Quiver.Path.cons q f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
[PROOFSTEP]
exact this
[GOAL]
case H.cons.a
V : Type u
inst✝ : Quiver V
X Y a b : Paths (Quiver.Symmetrify V)
q : Quiver.Path X a
f : a ⟶ b
ih : EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
[PROOFSTEP]
exact ih
[GOAL]
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ p) = Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
[PROOFSTEP]
nth_rw 2 [← Quiver.Path.reverse_reverse p]
[GOAL]
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (Quotient.CompClosure redStep) (Quiver.Path.reverse p ≫ Quiver.Path.reverse (Quiver.Path.reverse p)) =
    Quot.mk (Quotient.CompClosure redStep) (𝟙 Y)
[PROOFSTEP]
apply congr_comp_reverse
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ ∀ (x y : Paths (Quiver.Symmetrify V)) (f₁ f₂ : x ⟶ y),
    redStep f₁ f₂ → (Paths.lift (Quiver.Symmetrify.lift φ)).map f₁ = (Paths.lift (Quiver.Symmetrify.lift φ)).map f₂
[PROOFSTEP]
rintro _ _ _ _
  ⟨X, Y, f⟩
      -- Porting note: `simp` does not work, so manually `rewrite`
[GOAL]
case step
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
X✝ Y✝ : Paths (Quiver.Symmetrify V)
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ (Paths.lift (Quiver.Symmetrify.lift φ)).map (𝟙 (Paths.of.obj X)) =
    (Paths.lift (Quiver.Symmetrify.lift φ)).map (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f))
[PROOFSTEP]
erw [Paths.lift_nil, Paths.lift_cons, Quiver.Path.comp_nil, Paths.lift_toPath, Quiver.Symmetrify.lift_reverse]
[GOAL]
case step
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
X✝ Y✝ : Paths (Quiver.Symmetrify V)
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ 𝟙 ((Quiver.Symmetrify.lift φ).obj (Paths.of.obj X)) =
    (Quiver.Symmetrify.lift φ).map f ≫ Quiver.reverse ((Quiver.Symmetrify.lift φ).map f)
[PROOFSTEP]
symm
[GOAL]
case step
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
X✝ Y✝ : Paths (Quiver.Symmetrify V)
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ (Quiver.Symmetrify.lift φ).map f ≫ Quiver.reverse ((Quiver.Symmetrify.lift φ).map f) =
    𝟙 ((Quiver.Symmetrify.lift φ).obj (Paths.of.obj X))
[PROOFSTEP]
apply Groupoid.comp_inv
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ of V ⋙q (lift φ).toPrefunctor = φ
[PROOFSTEP]
rw [of_eq, Prefunctor.comp_assoc, Prefunctor.comp_assoc, Functor.toPrefunctor_comp]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ lift φ).toPrefunctor) = φ
[PROOFSTEP]
dsimp [lift]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ Quiver.Symmetrify.of ⋙q
      (Paths.of ⋙q
        (Quotient.functor redStep ⋙
            Quotient.lift redStep (Paths.lift (Quiver.Symmetrify.lift φ))
              (_ :
                ∀ (x y : Paths (Quiver.Symmetrify V)) (f₁ f₂ : x ⟶ y),
                  redStep f₁ f₂ →
                    (Paths.lift (Quiver.Symmetrify.lift φ)).map f₁ =
                      (Paths.lift (Quiver.Symmetrify.lift φ)).map f₂)).toPrefunctor) =
    φ
[PROOFSTEP]
rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ
[PROOFSTEP]
apply Quotient.lift_unique
[GOAL]
case hΦ
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Quotient.functor redStep ⋙ Φ = Paths.lift (Quiver.Symmetrify.lift φ)
[PROOFSTEP]
apply Paths.lift_unique
[GOAL]
case hΦ.hΦ
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor = Quiver.Symmetrify.lift φ
[PROOFSTEP]
fapply @Quiver.Symmetrify.lift_unique _ _ _ _ _ _ _ _ _
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor) = φ
[PROOFSTEP]
rw [← Functor.toPrefunctor_comp]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Quiver.Symmetrify.of ⋙q (Paths.of ⋙q ((Quotient.functor redStep).toPrefunctor ⋙q Φ.toPrefunctor)) = φ
[PROOFSTEP]
exact hΦ
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ ∀ {X Y : Quiver.Symmetrify V} (f : X ⟶ Y),
    (Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (Quiver.reverse f) =
      Quiver.reverse ((Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)
[PROOFSTEP]
rintro X Y f
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ (Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (Quiver.reverse f) =
    Quiver.reverse ((Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)
[PROOFSTEP]
simp only [← Functor.toPrefunctor_comp, Prefunctor.comp_map, Paths.of_map, inv_eq_inv]
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath (Quiver.reverse f))) =
    Quiver.reverse (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
[PROOFSTEP]
change
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
⊢ Φ.map (inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
[PROOFSTEP]
have := Functor.map_inv Φ ((Quotient.functor redStep).toPrefunctor.map f.toPath)
[GOAL]
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
this :
  Φ.map (CategoryTheory.inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
⊢ Φ.map (inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2.h.e'_8
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
this :
  Φ.map (CategoryTheory.inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
⊢ inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f)) =
    CategoryTheory.inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))
[PROOFSTEP]
simp only [inv_eq_inv]
[GOAL]
case h.e'_3
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Quiver.Symmetrify V
f : X ⟶ Y
this :
  Φ.map (CategoryTheory.inv ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
⊢ inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f))) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map (Quiver.Hom.toPath f)))
[PROOFSTEP]
simp only [inv_eq_inv]
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
⊢ freeGroupoidFunctor (𝟭q V) = 𝟭 (FreeGroupoid V)
[PROOFSTEP]
dsimp only [freeGroupoidFunctor]
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
⊢ lift (𝟭q V ⋙q of V) = 𝟭 (FreeGroupoid V)
[PROOFSTEP]
symm
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
⊢ 𝟭 (FreeGroupoid V) = lift (𝟭q V ⋙q of V)
[PROOFSTEP]
apply lift_unique
[GOAL]
case hΦ
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
⊢ of V ⋙q (𝟭 (FreeGroupoid V)).toPrefunctor = 𝟭q V ⋙q of V
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ freeGroupoidFunctor (φ ⋙q φ') = freeGroupoidFunctor φ ⋙ freeGroupoidFunctor φ'
[PROOFSTEP]
dsimp only [freeGroupoidFunctor]
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q φ' ⋙q of V'') = lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')
[PROOFSTEP]
symm
[GOAL]
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')
[PROOFSTEP]
apply lift_unique
[GOAL]
case hΦ
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''
[PROOFSTEP]
rfl
