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) = φ
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ✝ φ : V ⥤q V'
⊢ of V ⋙q (lift φ).toPrefunctor = φ
rw [of_eq, Prefunctor.comp_assoc, Prefunctor.comp_assoc, Functor.toPrefunctor_comp]
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) =
    φ
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) = φ
dsimp [lift]
no goals
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) =
    φ
rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]