-- Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
theorem congr_reverse {X Y : Paths <| Quiver.Symmetrify V} (p q : X ⟶ Y) :
    Quotient.CompClosure redStep p q → Quotient.CompClosure redStep p.reverse q.reverse

Proof state:
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 ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ Quiver.Path.reverse XW)
⊢ Quotient.CompClosure redStep (Quiver.Path.reverse (XW ≫ 𝟙 (Paths.of.obj X✝) ≫ WY))
    (Quiver.Path.reverse (XW ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ WY))

Tactic:
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

Result:
no goals

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

Tactic:
rintro ⟨XW, pp, qq, WY, _, Z, f⟩

Result:
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 ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ WY))

Proof state:
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 ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ Quiver.Path.reverse XW)

Tactic:
constructor

Result:
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✝)) (f.toPath ≫ (Quiver.reverse f).toPath)

Proof state:
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✝)) (f.toPath ≫ (Quiver.reverse f).toPath)

Tactic:
constructor

Result:
no goals

Proof state:
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 ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ WY))

Tactic:
have : Quotient.CompClosure redStep (WY.reverse ≫ 𝟙 _ ≫ XW.reverse)
    (WY.reverse ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ XW.reverse) := by
  constructor
  constructor

Result:
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 ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ Quiver.Path.reverse XW)
⊢ Quotient.CompClosure redStep (Quiver.Path.reverse (XW ≫ 𝟙 (Paths.of.obj X✝) ≫ WY))
    (Quiver.Path.reverse (XW ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ WY))