awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
fib : (c : C) → Functor.{v₂, v_1, u₂, u_1} (↑(F.obj c) : Type u₂) E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom ⋯
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) = hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom ⋯
c : C
X Y : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
⊢ (ι F c ⋙ functorFrom fib (fun {c c' : C} ↦ hom) hom_id hom_comp).map f ≫
      Iso.hom
        ((fun (x : (↑(F.obj c) : Type u₂)) ↦
            (Iso.refl ((ι F c ⋙ functorFrom fib (fun {c c' : C} ↦ hom) hom_id hom_comp).obj x) :
              (ι F c ⋙ functorFrom fib (fun {c c' : C} ↦ hom) hom_id hom_comp).obj x ≅
                (ι F c ⋙ functorFrom fib (fun {c c' : C} ↦ hom) hom_id hom_comp).obj x))
          Y) =
    Iso.hom
        ((fun (x : (↑(F.obj c) : Type u₂)) ↦
            (Iso.refl ((ι F c ⋙ functorFrom fib (fun {c c' : C} ↦ hom) hom_id hom_comp).obj x) :
              (ι F c ⋙ functorFrom fib (fun {c c' : C} ↦ hom) hom_id hom_comp).obj x ≅
                (ι F c ⋙ functorFrom fib (fun {c c' : C} ↦ hom) hom_id hom_comp).obj x))
          X) ≫
      (fib c).map f

Tactic:
simp [hom_id]
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
F' : C ⥤ Cat
α : F ⟶ F'
c : C
X Y : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
⊢ (ι F c ⋙ map α).map f ≫
      Iso.hom
        ((fun (X : (↑(F.obj c) : Type u₂)) ↦
            (Iso.refl ((ι F c ⋙ map α).obj X) : (ι F c ⋙ map α).obj X ≅ (ι F c ⋙ map α).obj X))
          Y) =
    Iso.hom
        ((fun (X : (↑(F.obj c) : Type u₂)) ↦
            (Iso.refl ((ι F c ⋙ map α).obj X) : (ι F c ⋙ map α).obj X ≅ (ι F c ⋙ map α).obj X))
          X) ≫
      ((α.app c).toFunctor ⋙ ι F' c).map f

Tactic:
simp [map]

Premises used: CategoryTheory.Grothendieck.map
-- Module: Mathlib.CategoryTheory.Groupoid.Basic
Goal:
C : Type u_1
inst : Groupoid.{u_2, u_1} C
⊢ Quiver.IsThin.{u_1, u_2} C ↔ ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)

Tactic:
⟨fun h c => h c c, fun h c d => Subsingleton.intro fun f g => ?_⟩

Premises used: Subsingleton.intro, Iff.intro
-- Module: Mathlib.CategoryTheory.Groupoid.Basic
Goal:
C : Type u_1
inst : Groupoid.{u_2, u_1} C
refine : ∀ (h : ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)) (c d : C) (f g : c ⟶ d), f = g
⊢ Quiver.IsThin.{u_1, u_2} C ↔ ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)

Tactic:
refine ⟨fun h c => h c c, fun h c d => Subsingleton.intro fun f g => ?_⟩
-- Module: Mathlib.CategoryTheory.Groupoid.Basic
Goal:
C : Type u_1
inst : Groupoid.{u_2, u_1} C
h : ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)
c d : C
f g : c ⟶ d
⊢ Subsingleton.{u_2 + 1} (d ⟶ d)

Tactic:
haveI := h d
-- Module: Mathlib.CategoryTheory.Groupoid.Basic
Goal:
C : Type u_1
inst : Groupoid.{u_2, u_1} C
h : ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton.{u_2 + 1} (d ⟶ d)
⊢ f = f ≫ inv g ≫ g

Tactic:
simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Basic
Goal:
C : Type u_1
inst : Groupoid.{u_2, u_1} C
h : ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton.{u_2 + 1} (d ⟶ d)
e_a : inv g ≫ g = inv f ≫ g
⊢ f ≫ inv g ≫ g = f ≫ inv f ≫ g

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Groupoid.Basic
Goal:
C : Type u_1
inst : Groupoid.{u_2, u_1} C
h : ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton.{u_2 + 1} (d ⟶ d)
⊢ inv g ≫ g = inv f ≫ g

Tactic:
simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Groupoid.inv_eq_inv, eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Groupoid.Basic
Goal:
C : Type u_1
inst : Groupoid.{u_2, u_1} C
h : ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton.{u_2 + 1} (d ⟶ d)
⊢ f ≫ inv f ≫ g = g

Tactic:
simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]

Premises used: CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Basic
Goal:
C : Type u_1
inst : Groupoid.{u_2, u_1} C
h : ∀ (c : C), Subsingleton.{u_2 + 1} (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton.{u_2 + 1} (d ⟶ d)
f₁ : f = f ≫ inv g ≫ g
f₂ : f ≫ inv g ≫ g = f ≫ inv f ≫ g
f₃ : f ≫ inv f ≫ g = g
⊢ f = g

Tactic:
calc
    f = f ≫ inv g ≫ g := by simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]
    _ = f ≫ inv f ≫ g := by congr 1
                            simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]
    _ = g := by simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]

Premises used: CategoryTheory.Groupoid.inv
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V_1 : Type u
inst : Quiver.{v, u} V_1
V : Type u_1
inst_1 : Quiver.{u_2, u_1} V
inst_2 : Nonempty V
inhabit : ∀ (inhabited_h : Inhabited V), Nonempty.{u_1 + 1} (Quiver.FreeGroupoid.{u_1, u_2} V)
⊢ Nonempty.{u_1 + 1} (Quiver.FreeGroupoid.{u_1, u_2} V)

Tactic:
inhabit V
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V_1 : Type u
inst : Quiver.{v, u} V_1
V : Type u_1
inst_1 : Quiver.{u_2, u_1} V
inst_2 : Nonempty V
inhabited_h : Inhabited V
⊢ Nonempty.{u_1 + 1} (Quiver.FreeGroupoid.{u_1, u_2} V)

Tactic:
⟨⟨@default V _⟩⟩

Premises used: Inhabited.default, Nonempty.intro, CategoryTheory.Quotient.mk
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V_1 : Type u
inst : Quiver.{v, u} V_1
V : Type u_1
inst_1 : Quiver.{u_2, u_1} V
inst_2 : Nonempty V
inhabited_h : Inhabited V
⊢ Nonempty.{u_1 + 1} (Quiver.FreeGroupoid.{u_1, u_2} V)

Tactic:
exact ⟨⟨@default V _⟩⟩
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X_1 Y_1 X_2 Y_2 X Y : Paths (Symmetrify V)
X_3 Z : Symmetrify V
f : X_3 ⟶ Z
XW : X_1 ⟶ Prefunctor.obj (Paths.of (Symmetrify V)) X_3
WY : Prefunctor.obj (Paths.of (Symmetrify V)) X_3 ⟶ Y_1
h : redStep.{u, v} (𝟙 (Prefunctor.obj (Paths.of (Symmetrify V)) X_3)) (f.toPath ≫ (reverse f).toPath)
⊢ HomRel.CompClosure redStep (X := Y_1) (Y := X_1)
    (Path.reverse WY ≫ 𝟙 (Prefunctor.obj (Paths.of (Symmetrify V)) X_3) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X_1 Y_1 X_2 Y_2 X Y : Paths (Symmetrify V)
X_3 Z : Symmetrify V
f : X_3 ⟶ Z
XW : X_1 ⟶ Prefunctor.obj (Paths.of (Symmetrify V)) X_3
WY : Prefunctor.obj (Paths.of (Symmetrify V)) X_3 ⟶ Y_1
⊢ redStep.{u, v} (𝟙 (Prefunctor.obj (Paths.of (Symmetrify V)) X_3)) (f.toPath ≫ (reverse f).toPath)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X_1 Y_1 X_2 Y_2 X Y : Paths (Symmetrify V)
X_3 Z : Symmetrify V
f : X_3 ⟶ Z
XW : X_1 ⟶ Prefunctor.obj (Paths.of (Symmetrify V)) X_3
WY : Prefunctor.obj (Paths.of (Symmetrify V)) X_3 ⟶ Y_1
⊢ HomRel.CompClosure redStep (X := Y_1) (Y := X_1)
    (Path.reverse WY ≫ 𝟙 (Prefunctor.obj (Paths.of (Symmetrify V)) X_3) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)

Tactic:
have : HomRel.CompClosure redStep (WY.reverse ≫ 𝟙 _ ≫ XW.reverse)
      (WY.reverse ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ XW.reverse) := by
    constructor
    constructor
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X_1 Y_1 X_2 Y_2 X Y : Paths (Symmetrify V)
X_3 Z : Symmetrify V
f : X_3 ⟶ Z
XW : X_1 ⟶ Prefunctor.obj (Paths.of (Symmetrify V)) X_3
WY : Prefunctor.obj (Paths.of (Symmetrify V)) X_3 ⟶ Y_1
this :
  HomRel.CompClosure redStep (X := Y_1) (Y := X_1)
    (Path.reverse WY ≫ 𝟙 (Prefunctor.obj (Paths.of (Symmetrify V)) X_3) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)
⊢ HomRel.CompClosure redStep (Path.reverse (XW ≫ 𝟙 (Prefunctor.obj (Paths.of (Symmetrify V)) X_3) ≫ WY))
    (Path.reverse (XW ≫ (f.toPath ≫ (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

Premises used: Quiver.reverse_reverse, CategoryTheory.CategoryStruct.id, Quiver.Path.nil_comp, Quiver.Path.reverse_comp, Quiver.Path.comp_assoc, Quiver.Path.reverse, CategoryTheory.CategoryStruct.comp, Quiver.Path.reverse_toPath
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
H : EqvGen (HomRel.CompClosure redStep) (p ≫ Path.reverse p) (𝟙 X)
⊢ Eq (α := Quot (α := X ⟶ X) (HomRel.CompClosure redStep)) (Quot.mk (HomRel.CompClosure redStep) (p ≫ Path.reverse p))
    (Quot.mk (HomRel.CompClosure redStep) (𝟙 X))

Tactic:
apply Quot.eqvGen_sound

Premises used: Quot.eqvGen_sound
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y : Paths (Symmetrify V)
⊢ EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (Path.nil ≫ Path.reverse Path.nil) (𝟙 X)

Tactic:
apply EqvGen.refl

Premises used: Relation.EqvGen.refl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
H : X ⟶ X
H₁ : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q.cons f ≫ (reverse f).toPath.comp q.reverse) (q ≫ q.reverse)
H₂ : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q.cons f ≫ (reverse f).toPath.comp q.reverse) (𝟙 X)

Tactic:
fapply EqvGen.trans

Premises used: Relation.EqvGen.trans
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ X ⟶ X

Tactic:
exact q ≫ Quiver.Path.reverse q
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
H : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath.comp q.reverse)
⊢ EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q.cons f ≫ (reverse f).toPath.comp q.reverse) (q ≫ q.reverse)

Tactic:
apply EqvGen.symm

Premises used: Relation.EqvGen.symm
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
H :
  HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
    (q.cons f ≫ (reverse f).toPath.comp q.reverse)
⊢ EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath.comp q.reverse)

Tactic:
apply EqvGen.rel

Premises used: Relation.EqvGen.rel
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
h : redStep.{u, v} (𝟙 b) (f.toPath ≫ (reverse f).toPath)
⊢ HomRel.CompClosure redStep (X := X) (Y := X) (q ≫ 𝟙 b ≫ q.reverse) (q ≫ (f.toPath ≫ (reverse f).toPath) ≫ q.reverse)

Tactic:
apply HomRel.CompClosure.intro

Premises used: CategoryTheory.HomRel.CompClosure.intro
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ redStep.{u, v} (𝟙 b) (f.toPath ≫ (reverse f).toPath)

Tactic:
apply redStep.step

Premises used: Quiver.FreeGroupoid.redStep.step
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ HomRel.CompClosure redStep (X := X) (Y := X) (q ≫ 𝟙 b ≫ q.reverse) (q ≫ (f.toPath ≫ (reverse f).toPath) ≫ q.reverse)

Tactic:
have : HomRel.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
          (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫
            Quiver.Path.reverse q) := by
        apply HomRel.CompClosure.intro
        apply redStep.step
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this :
  HomRel.CompClosure redStep (X := X) (Y := X) (q ≫ 𝟙 b ≫ q.reverse) (q ≫ (f.toPath ≫ (reverse f).toPath) ≫ q.reverse)
⊢ HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
    (q ≫ f.toPath ≫ (reverse f).toPath ≫ q.reverse)

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this :
  HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
    (q ≫ f.toPath ≫ (reverse f).toPath ≫ q.reverse)
H :
  ∀
    (this :
      HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
        (((q ≫ f.toPath) ≫ (reverse f).toPath) ≫ q.reverse)),
    HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
      ((q.cons f ≫ (reverse f).toPath) ≫ q.reverse)
⊢ HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
    (q.cons f ≫ (reverse f).toPath ≫ q.reverse)

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

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this :
  HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
    (((q ≫ f.toPath) ≫ (reverse f).toPath) ≫ q.reverse)
⊢ HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
    ((q.cons f ≫ (reverse f).toPath) ≫ q.reverse)

Tactic:
this

Premises used: Quiver.Hom.toPath, Quiver.Path.comp
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this :
  HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
    (((q ≫ f.toPath) ≫ (reverse f).toPath) ≫ q.reverse)
⊢ HomRel.CompClosure (C := Paths (Symmetrify V)) redStep (X := X) (Y := X) (q ≫ q.reverse)
    ((q.cons f ≫ (reverse f).toPath) ≫ q.reverse)

Tactic:
exact this
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)

Tactic:
ih
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y b c : Paths (Symmetrify V)
q : Path.{v, u} X b
f : b ⟶ c
ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)

Tactic:
exact ih
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
H : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (Path.nil ≫ Path.reverse Path.nil) (𝟙 X)
H₁ :
  ∀ {b c : Paths (Symmetrify V)} (q : Path.{v, u} X b) (f : b ⟶ c)
    (ih : EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)),
    EqvGen (α := X ⟶ X) (HomRel.CompClosure redStep) (q.cons f ≫ (q.cons f).reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) (p ≫ Path.reverse p) (𝟙 X)

Tactic:
induction p with
  | nil => apply EqvGen.refl
  | cons q f ih =>
    simp only [Quiver.Path.reverse]
    fapply EqvGen.trans
    -- Porting note: dot notation for `Quiver.Path.*` and `Quiver.Hom.*` not working
    · exact q ≫ Quiver.Path.reverse q
    · apply EqvGen.symm
      apply EqvGen.rel
      have : HomRel.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
          (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫
            Quiver.Path.reverse q) := by
        apply HomRel.CompClosure.intro
        apply redStep.step
      simp only [Category.assoc, Category.id_comp] at this ⊢
      -- Porting note: `simp` cannot see how `Quiver.Path.comp_assoc` is relevant, so change to
      -- category notation
      change HomRel.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 ⊢
      exact this
    · exact ih

Premises used: CategoryTheory.Category.assoc, Relation.EqvGen.trans, Relation.EqvGen.refl, Quiver.Path.reverse, Relation.EqvGen.rel, Relation.EqvGen.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
nth_rw :
  Eq (α := Quot (α := Y ⟶ Y) (HomRel.CompClosure redStep))
    (Quot.mk (HomRel.CompClosure redStep) (Path.reverse p ≫ (Path.reverse p).reverse))
    (Quot.mk (HomRel.CompClosure redStep) (𝟙 Y))
⊢ Eq (α := Quot (α := Y ⟶ Y) (HomRel.CompClosure redStep)) (Quot.mk (HomRel.CompClosure redStep) (Path.reverse p ≫ p))
    (Quot.mk (HomRel.CompClosure redStep) (𝟙 Y))

Tactic:
nth_rw 2 [← Quiver.Path.reverse_reverse p]

Premises used: Quiver.Path.reverse_reverse
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ Eq (α := Quot (α := Y ⟶ Y) (HomRel.CompClosure redStep))
    (Quot.mk (HomRel.CompClosure redStep) (Path.reverse p ≫ (Path.reverse p).reverse))
    (Quot.mk (HomRel.CompClosure redStep) (𝟙 Y))

Tactic:
apply congr_comp_reverse

Premises used: Quiver.FreeGroupoid.congr_comp_reverse
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
⊢ Eq (α := V ⥤q Quiver.FreeGroupoid.{u, v} V) (of V)
    (Symmetrify.of ⋙q Paths.of (Symmetrify V) ⋙q Functor.toPrefunctor (Quotient.functor redStep))

Tactic:
rfl

Premises used: Prefunctor.comp, Quiver.FreeGroupoid, Quiver.Hom.toPath, Quiver.FreeGroupoid.of, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Groupoid.{u_1, u'} V'
φ : Prefunctor.{v, u_1, u, u'} V V'
X_1 Y_1 : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
erw :
  𝟙 ((Symmetrify.lift φ).obj (Prefunctor.obj (Paths.of (Symmetrify V)) X)) =
    (Symmetrify.lift φ).map f ≫ reverse ((Symmetrify.lift φ).map f)
⊢ (Paths.lift (Symmetrify.lift φ)).map (𝟙 (Prefunctor.obj (Paths.of (Symmetrify V)) X)) =
    (Paths.lift (Symmetrify.lift φ)).map (f.toPath ≫ (reverse f).toPath)

Tactic:
erw [Paths.lift_nil, Paths.lift_cons, Quiver.Path.comp_nil, Paths.lift_toPath,
      Quiver.Symmetrify.lift_reverse]

Premises used: Quiver.Symmetrify.lift_reverse, CategoryTheory.Paths.lift_cons, Quiver.Path.comp_nil, CategoryTheory.Paths.lift_toPath, CategoryTheory.Paths.lift_nil
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Groupoid.{u_1, u'} V'
φ : Prefunctor.{v, u_1, u, u'} V V'
X_1 Y_1 : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
symm :
  (Symmetrify.lift φ).map f ≫ reverse ((Symmetrify.lift φ).map f) =
    𝟙 ((Symmetrify.lift φ).obj (Prefunctor.obj (Paths.of (Symmetrify V)) X))
⊢ 𝟙 ((Symmetrify.lift φ).obj (Prefunctor.obj (Paths.of (Symmetrify V)) X)) =
    (Symmetrify.lift φ).map f ≫ reverse ((Symmetrify.lift φ).map f)

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Groupoid.{u_1, u'} V'
φ : Prefunctor.{v, u_1, u, u'} V V'
X_1 Y_1 : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
⊢ (Symmetrify.lift φ).map f ≫ reverse ((Symmetrify.lift φ).map f) =
    𝟙 ((Symmetrify.lift φ).obj (Prefunctor.obj (Paths.of (Symmetrify V)) X))

Tactic:
apply Groupoid.comp_inv

Premises used: CategoryTheory.Groupoid.comp_inv
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Groupoid.{u_1, u'} V'
φ : Prefunctor.{v, u_1, u, u'} V V'
rw : Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ lift φ).toPrefunctor) = φ
⊢ of V ⋙q (lift φ).toPrefunctor = φ

Tactic:
rw [of_eq, Prefunctor.comp_assoc, Prefunctor.comp_assoc, Functor.toPrefunctor_comp]

Premises used: Prefunctor.comp_assoc, CategoryTheory.Functor.toPrefunctor_comp, Quiver.FreeGroupoid.of_eq
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Groupoid.{u_1, u'} V'
φ : Prefunctor.{v, u_1, u, u'} V V'
rw : Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Paths.lift (Symmetrify.lift φ)).toPrefunctor) = φ
rw₁ : Symmetrify.of ⋙q Symmetrify.lift φ = φ
rw₂ rw₃ : φ = φ
⊢ Symmetrify.of ⋙q
      (Paths.of (Symmetrify V) ⋙q
        (Quotient.functor redStep ⋙
            CategoryTheory.Quotient.lift redStep (Paths.lift (Symmetrify.lift φ)) ⋯).toPrefunctor) =
    φ

Tactic:
rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]

Premises used: Quiver.Symmetrify.lift_spec, CategoryTheory.Paths.lift_spec, CategoryTheory.Quotient.lift_spec
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Groupoid.{u_1, u'} V'
φ : Prefunctor.{v, u_1, u, u'} V V'
Φ : Quiver.FreeGroupoid.{u, v} V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
hΦ₁ : Quotient.functor redStep ⋙ Φ = Paths.lift (Symmetrify.lift φ)
⊢ Φ = lift φ

Tactic:
apply Quotient.lift_unique

Premises used: CategoryTheory.Quotient.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Groupoid.{u_1, u'} V'
φ : Prefunctor.{v, u_1, u, u'} V V'
Φ : Quiver.FreeGroupoid.{u, v} V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
hΦ₁ : Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor = Symmetrify.lift φ
⊢ Quotient.functor redStep ⋙ Φ = Paths.lift (Symmetrify.lift φ)

Tactic:
apply Paths.lift_unique

Premises used: CategoryTheory.Paths.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Groupoid.{u_1, u'} V'
φ : Prefunctor.{v, u_1, u, u'} V V'
Φ : Quiver.FreeGroupoid.{u, v} V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
fapply : Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor) = φ
fapply₁ :
  ∀ {X Y : Symmetrify V} (f : X ⟶ Y),
    (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (reverse f) =
      reverse ((Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)
⊢ Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor = Symmetrify.lift φ

Tactic:
fapply @Quiver.Symmetrify.lift_unique _ _ _ _ _ _ _ _ _

Premises used: Quiver.Symmetrify.lift_unique