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))
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)
rintro ⟨XW, pp, qq, WY, _, Z, f⟩
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))
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))
have : Quotient.CompClosure redStep (WY.reverse ≫ 𝟙 _ ≫ XW.reverse)
    (WY.reverse ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ XW.reverse) := by
  constructor
  constructor
no goals
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))
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
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))
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)
constructor
no goals
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))
constructor