-- Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
theorem congr_comp_reverse {X Y : Paths <| Quiver.Symmetrify V} (p : X ⟶ Y) :
    Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (p ≫ p.reverse) =
      Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (𝟙 X)

Proof state:
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 ≫ q.reverse) (𝟙 X)
⊢ redStep (𝟙 a) (f.toPath ≫ (Quiver.reverse f).toPath)

Tactic:
apply redStep.step

Result:
no goals

Proof state:
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 ≫ q.reverse) (𝟙 X)
this : Quotient.CompClosure redStep (q ≫ q.reverse) (q ≫ f.toPath ≫ (Quiver.reverse f).toPath ≫ q.reverse)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath ≫ q.reverse)

Tactic:
simp only [← Category.assoc] at this ⊢

Result:
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 ≫ q.reverse) (𝟙 X)
this : Quotient.CompClosure redStep (q ≫ q.reverse) (((q ≫ f.toPath) ≫ (Quiver.reverse f).toPath) ≫ q.reverse)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) ((q.cons f ≫ (Quiver.reverse f).toPath) ≫ q.reverse)

Proof state:
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 ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)

Tactic:
exact ih

Result:
no goals

Proof state:
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 ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q.cons f ≫ (q.cons f).reverse) (𝟙 X)

Tactic:
simp only [Quiver.Path.reverse]

Result:
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 ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse) (𝟙 X)

Proof state:
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 ≫ q.reverse) (𝟙 X)
this : Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ q.reverse) (q ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ q.reverse)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse)

Tactic:
simp only [Category.assoc, Category.id_comp] at this ⊢

Result:
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 ≫ q.reverse) (𝟙 X)
this : Quotient.CompClosure redStep (q ≫ q.reverse) (q ≫ f.toPath ≫ (Quiver.reverse f).toPath ≫ q.reverse)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse)

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

Tactic:
apply Quot.eqvGen_sound

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

Proof state:
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 ≫ q.reverse) (𝟙 X)
this : Quotient.CompClosure redStep (q ≫ q.reverse) (((q ≫ f.toPath) ≫ (Quiver.reverse f).toPath) ≫ q.reverse)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) ((q.cons f ≫ (Quiver.reverse f).toPath) ≫ q.reverse)

Tactic:
exact this

Result:
no goals

Proof state:
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 ≫ q.reverse) (𝟙 X)
this : Quotient.CompClosure redStep (q ≫ q.reverse) (q ≫ f.toPath ≫ (Quiver.reverse f).toPath ≫ q.reverse)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse)

Tactic:
change Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
  (Quiver.Path.cons q f ≫ (Quiver.Hom.toPath (Quiver.reverse f)) ≫ (Quiver.Path.reverse q))

Result:
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 ≫ q.reverse) (𝟙 X)
this : Quotient.CompClosure redStep (q ≫ q.reverse) (q ≫ f.toPath ≫ (Quiver.reverse f).toPath ≫ q.reverse)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath ≫ q.reverse)

Proof state:
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 ≫ q.reverse) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ q.reverse) (q ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ q.reverse)

Tactic:
apply Quotient.CompClosure.intro

Result:
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 ≫ q.reverse) (𝟙 X)
⊢ redStep (𝟙 a) (f.toPath ≫ (Quiver.reverse f).toPath)

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

Tactic:
induction' p with a b q f ih

Result:
case H.nil
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.nil ≫ Quiver.Path.nil.reverse) (𝟙 X)

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 ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q.cons f ≫ (q.cons f).reverse) (𝟙 X)

Proof state:
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 ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse)

Tactic:
apply EqvGen.rel

Result:
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 ≫ q.reverse) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse)

Proof state:
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 ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse) (q ≫ q.reverse)

Tactic:
apply EqvGen.symm

Result:
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 ≫ q.reverse) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ q.reverse) (q.cons f ≫ (Quiver.reverse f).toPath.comp q.reverse)

Proof state:
case H.nil
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.nil ≫ Quiver.Path.nil.reverse) (𝟙 X)

Tactic:
apply EqvGen.refl

Result:
no goals