-- Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
theorem lift_unique (φ : V ⥤q V') (Φ : FreeGroupoid V ⥤ V') (hΦ : of V ⋙q Φ.toPrefunctor = φ) :
    Φ = lift φ

Proof state:
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) = φ

Tactic:
rw [← Functor.toPrefunctor_comp]

Result:
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)) = φ

Proof state:
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 f.toPath)) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map f.toPath))
⊢ Φ.map (inv ((Quotient.functor redStep).map f.toPath)) = inv (Φ.map ((Quotient.functor redStep).map f.toPath))

Tactic:
convert this <;> simp only [inv_eq_inv]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ

Tactic:
apply Quotient.lift_unique

Result:
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 φ)

Proof state:
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.reverse f).toPath) =
    Quiver.reverse (Φ.map ((Quotient.functor redStep).map f.toPath))

Tactic:
change Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
  inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))

Result:
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 f.toPath)) = inv (Φ.map ((Quotient.functor redStep).map f.toPath))

Proof state:
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)) = φ

Tactic:
exact hΦ

Result:
no goals

Proof state:
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 φ

Tactic:
fapply @Quiver.Symmetrify.lift_unique _ _ _ _ _ _ _ _ _

Result:
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) = φ

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)

Proof state:
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)

Tactic:
rintro X Y f

Result:
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)

Proof state:
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)

Tactic:
simp only [← Functor.toPrefunctor_comp, Prefunctor.comp_map, Paths.of_map, inv_eq_inv]

Result:
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.reverse f).toPath) =
    Quiver.reverse (Φ.map ((Quotient.functor redStep).map f.toPath))

Proof state:
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 f.toPath)) = inv (Φ.map ((Quotient.functor redStep).map f.toPath))

Tactic:
have := Functor.map_inv Φ ((Quotient.functor redStep).toPrefunctor.map f.toPath)

Result:
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 f.toPath)) =
    CategoryTheory.inv (Φ.map ((Quotient.functor redStep).map f.toPath))
⊢ Φ.map (inv ((Quotient.functor redStep).map f.toPath)) = inv (Φ.map ((Quotient.functor redStep).map f.toPath))

Proof state:
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 φ)

Tactic:
apply Paths.lift_unique

Result:
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 φ