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)
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)
apply Quot.EqvGen_sound
case H.nil
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.nil ≫ Quiver.Path.reverse Quiver.Path.nil) (𝟙 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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.cons q f ≫ Quiver.Path.reverse (Quiver.Path.cons q f)) (𝟙 X)
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)
induction' p with a b q f ih
no goals
case H.nil
V : Type u
inst✝ : Quiver V
X Y : Paths (Quiver.Symmetrify V)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.nil ≫ Quiver.Path.reverse Quiver.Path.nil) (𝟙 X)
apply EqvGen.refl
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q)) (𝟙 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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (Quiver.Path.cons q f ≫ Quiver.Path.reverse (Quiver.Path.cons q f)) (𝟙 X)
simp only [Quiver.Path.reverse]
case H.cons.y
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ X ⟶ X

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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q)) ?H.cons.y

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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) ?H.cons.y (𝟙 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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q)) (𝟙 X)
fapply EqvGen.trans
no goals
case H.cons.y
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ X ⟶ X
exact q ≫ Quiver.Path.reverse q
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
    (q ≫ Quiver.Path.reverse q)
apply EqvGen.symm
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
apply EqvGen.rel
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 ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
have : Quotient.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫
      Quiver.Path.reverse q) := by
  apply Quotient.CompClosure.intro
  apply redStep.step
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 ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (q ≫ Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
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 ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
simp only [Category.assoc, Category.id_comp] at this ⊢
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 ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (q ≫ Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
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 ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (q ≫ Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Path.comp (Quiver.Hom.toPath (Quiver.reverse f)) (Quiver.Path.reverse q))
change Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
  (Quiver.Path.cons q f ≫ (Quiver.Hom.toPath (Quiver.reverse f)) ≫ (Quiver.Path.reverse q))
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 ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (((q ≫ Quiver.Hom.toPath f) ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    ((Quiver.Path.cons q f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
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 ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (q ≫ Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (Quiver.Path.cons q f ≫ Quiver.Hom.toPath (Quiver.reverse f) ≫ Quiver.Path.reverse q)
simp only [←Category.assoc] at this ⊢
no goals
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 ≫ Quiver.Path.reverse q) (𝟙 X)
this :
  Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    (((q ≫ Quiver.Hom.toPath f) ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
⊢ Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
    ((Quiver.Path.cons q f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
exact this
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ redStep (𝟙 a) (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f))
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ Quotient.CompClosure redStep (q ≫ 𝟙 a ≫ Quiver.Path.reverse q)
    (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q)
apply Quotient.CompClosure.intro
no goals
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ redStep (𝟙 a) (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f))
apply redStep.step
no goals
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 ≫ Quiver.Path.reverse q) (𝟙 X)
⊢ EqvGen (Quotient.CompClosure redStep) (q ≫ Quiver.Path.reverse q) (𝟙 X)
exact ih