awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = φ
rw :
  Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Functor.toPrefunctor (Quotient.functor redStep) ⋙q Φ.toPrefunctor)) = φ
⊢ Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor) = φ

Tactic:
rw [← Functor.toPrefunctor_comp]

Premises used: CategoryTheory.Functor.toPrefunctor_comp
-- 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 = φ
⊢ Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Functor.toPrefunctor (Quotient.functor redStep) ⋙q Φ.toPrefunctor)) = φ

Tactic:
hΦ

Premises used: Prefunctor.comp, Quiver.Hom.toPath, Quiver.FreeGroupoid.of, Quiver.Symmetrify.of
-- 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 = φ
⊢ Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Functor.toPrefunctor (Quotient.functor redStep) ⋙q Φ.toPrefunctor)) = φ

Tactic:
exact hΦ
-- 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 = φ
X Y : Symmetrify V
f : X ⟶ Y
simp :
  Eq (α :=
    (Paths.of (Symmetrify V) ⋙q (Functor.toPrefunctor (Quotient.functor redStep) ⋙q Φ.toPrefunctor)).obj Y ⟶
      (Paths.of (Symmetrify V) ⋙q (Functor.toPrefunctor (Quotient.functor redStep) ⋙q Φ.toPrefunctor)).obj X)
    (Φ.toPrefunctor.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) (reverse f).toPath))
    (reverse (Φ.toPrefunctor.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
⊢ (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (reverse f) =
    reverse ((Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)

Tactic:
simp only [← Functor.toPrefunctor_comp, Prefunctor.comp_map, Paths.of_map]

Premises used: Prefunctor.comp_map, CategoryTheory.Functor.toPrefunctor_comp, CategoryTheory.Paths.of_map
-- 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 = φ
X Y : Symmetrify V
f : X ⟶ Y
change :
  Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Φ.map (Groupoid.inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (Groupoid.inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
⊢ Eq (α :=
    (Paths.of (Symmetrify V) ⋙q (Functor.toPrefunctor (Quotient.functor redStep) ⋙q Φ.toPrefunctor)).obj Y ⟶
      (Paths.of (Symmetrify V) ⋙q (Functor.toPrefunctor (Quotient.functor redStep) ⋙q Φ.toPrefunctor)).obj X)
    (Φ.toPrefunctor.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) (reverse f).toPath))
    (reverse (Φ.toPrefunctor.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))

Tactic:
change Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
      Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Groupoid.inv, CategoryTheory.Functor.map, Quiver.FreeGroupoid.redStep, Quiver.Hom.toPath, Prefunctor.map, CategoryTheory.Functor.toPrefunctor
-- 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 = φ
X Y : Symmetrify V
f : X ⟶ Y
⊢ Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Φ.map (inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))

Tactic:
have := Functor.map_inv Φ ((Quotient.functor redStep).toPrefunctor.map f.toPath)
-- 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 = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Φ.map (inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
⊢ Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Φ.map (inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))

Tactic:
this
-- 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 = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Φ.map (inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
h :
  Eq (α :=
    Hom (V := Quiver.FreeGroupoid.{u, v} V) (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y)
      (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Groupoid.inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath))
    (inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath))
h₁ :
  Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Groupoid.inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
⊢ Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Φ.map (Groupoid.inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (Groupoid.inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))

Tactic:
convert! this
-- 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 = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Φ.map (inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
⊢ Eq (α :=
    Hom (V := Quiver.FreeGroupoid.{u, v} V) (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y)
      (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Groupoid.inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath))
    (inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath))

Tactic:
simp only [Groupoid.inv_eq_inv]

Premises used: CategoryTheory.Groupoid.inv_eq_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'
Φ : Quiver.FreeGroupoid.{u, v} V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Φ.map (inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
⊢ Eq (α :=
    Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) Y) ⟶
      Φ.obj (Prefunctor.obj (Functor.toPrefunctor (Quotient.functor redStep)) X))
    (Groupoid.inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))

Tactic:
simp only [Groupoid.inv_eq_inv]

Premises used: CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
symm :
  Eq (α := Quiver.FreeGroupoid.{u, v} V ⥤ Quiver.FreeGroupoid.{u, v} V) (𝟭 (Quiver.FreeGroupoid.{u, v} V))
    (lift (𝟭q V ⋙q of V))
⊢ Eq (α := Quiver.FreeGroupoid.{u, v} V ⥤ Quiver.FreeGroupoid.{u, v} V) (lift (𝟭q V ⋙q of V))
    (𝟭 (Quiver.FreeGroupoid.{u, v} V))

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
hΦ :
  Eq (α := V ⥤q Quiver.FreeGroupoid.{u, v} V) (of V ⋙q Functor.toPrefunctor (𝟭 (Quiver.FreeGroupoid.{u, v} V)))
    (𝟭q V ⋙q of V)
⊢ Eq (α := Quiver.FreeGroupoid.{u, v} V ⥤ Quiver.FreeGroupoid.{u, v} V) (𝟭 (Quiver.FreeGroupoid.{u, v} V))
    (lift (𝟭q V ⋙q of V))

Tactic:
apply lift_unique

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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Quiver.{v', u'} V'
V'' : Type u''
inst_2 : Quiver.{v'', u''} V''
φ : Prefunctor.{v, v', u, u'} V V'
φ' : Prefunctor.{v', v'', u', u''} V' V''
symm : lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')
⊢ lift (φ ⋙q φ' ⋙q of V'') = lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Quiver.{v', u'} V'
V'' : Type u''
inst_2 : Quiver.{v'', u''} V''
φ : Prefunctor.{v, v', u, u'} V V'
φ' : Prefunctor.{v', v'', u', u''} V' V''
hΦ : of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''
⊢ lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')

Tactic:
apply lift_unique

Premises used: Quiver.FreeGroupoid.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Goal:
V : Type u
inst : Quiver.{v, u} V
V' : Type u'
inst_1 : Quiver.{v', u'} V'
V'' : Type u''
inst_2 : Quiver.{v'', u''} V''
φ : Prefunctor.{v, v', u, u'} V V'
φ' : Prefunctor.{v', v'', u', u''} V' V''
⊢ of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Nonempty C
⊢ Nonempty.{u + 1} (FreeGroupoid.{v, u} C)

Tactic:
⟨Quotient.mk (Quotient.mk ((Paths.of _).obj (Classical.arbitrary C)))⟩

Premises used: Nonempty.intro, Classical.arbitrary, CategoryTheory.Paths.of, CategoryTheory.Quotient.mk, Prefunctor.obj
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
X : FreeGroupoid.{v, u} C
⊢ X = mk (X.as (r := homRel C).as (r := Quiver.FreeGroupoid.redStep))

Tactic:
rfl

Premises used: CategoryTheory.FreeGroupoid, Quiver.FreeGroupoid, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 : C
h : Eq (α := FreeGroupoid.{v, u} C) (Functor.obj (of C) x) (Functor.obj (of C) x_1)
refl : x = x
⊢ x = x_1

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
x : C
⊢ x = x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
φ : Functor.{v, v₁, u, u₁} C G
x x_1 : Quiver.FreeGroupoid.{u, v} C
f g : x ⟶ x_1
r : homRel C f g
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) ⋯ ⋯ =
      φ.toPrefunctor.map f

Tactic:
have {X Y : C} (f : X ⟶ Y) :=
        Prefunctor.congr_hom (Quiver.FreeGroupoid.lift_spec φ.toPrefunctor) f
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
φ : Functor.{v, v₁, u, u₁} C G
x x_1 : Quiver.FreeGroupoid.{u, v} C
f g : x ⟶ x_1
r : homRel C f g
this :
  ∀ {X Y : C} (f : X ⟶ Y),
    Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) ⋯ ⋯ =
      φ.toPrefunctor.map f
map_id :
  ∀ (X : C),
    Eq (α :=
      (Quiver.FreeGroupoid.lift φ.toPrefunctor).obj (Prefunctor.obj (Quiver.FreeGroupoid.of C) X) ⟶
        (Quiver.FreeGroupoid.lift φ.toPrefunctor).obj (Prefunctor.obj (Quiver.FreeGroupoid.of C) X))
      ((Quiver.FreeGroupoid.lift φ.toPrefunctor).map (Prefunctor.map (Quiver.FreeGroupoid.of C) (𝟙 X)))
      ((Quiver.FreeGroupoid.lift φ.toPrefunctor).map (𝟙 (Prefunctor.obj (Quiver.FreeGroupoid.of C) X)))
map_comp :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    Eq (α :=
      (Quiver.FreeGroupoid.lift φ.toPrefunctor).obj (Prefunctor.obj (Quiver.FreeGroupoid.of C) X) ⟶
        (Quiver.FreeGroupoid.lift φ.toPrefunctor).obj (Prefunctor.obj (Quiver.FreeGroupoid.of C) Z))
      ((Quiver.FreeGroupoid.lift φ.toPrefunctor).map (Prefunctor.map (Quiver.FreeGroupoid.of C) (f ≫ g)))
      ((Quiver.FreeGroupoid.lift φ.toPrefunctor).map
        (Prefunctor.map (Quiver.FreeGroupoid.of C) f ≫ Prefunctor.map (Quiver.FreeGroupoid.of C) g))
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map f = (Quiver.FreeGroupoid.lift φ.toPrefunctor).map g

Tactic:
induction r
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
φ : Functor.{v, v₁, u, u₁} C G
change :
  Quiver.FreeGroupoid.of C ⋙q Functor.toPrefunctor (Quotient.functor (homRel C)) ⋙q (lift φ).toPrefunctor =
    φ.toPrefunctor
⊢ (of C ⋙ lift φ).toPrefunctor = φ.toPrefunctor

Tactic:
change Quiver.FreeGroupoid.of C ⋙q
      (Quotient.functor (FreeGroupoid.homRel C)).toPrefunctor ⋙q
        (lift φ).toPrefunctor = φ.toPrefunctor

Premises used: CategoryTheory.Quotient.functor, Quiver.FreeGroupoid.of, CategoryTheory.FreeGroupoid.homRel, CategoryTheory.Functor.toPrefunctor, CategoryTheory.FreeGroupoid.lift
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
φ : Functor.{v, v₁, u, u₁} C G
⊢ Quiver.FreeGroupoid.of C ⋙q Functor.toPrefunctor (Quotient.functor (homRel C)) ⋙q (lift φ).toPrefunctor =
    φ.toPrefunctor

Tactic:
simp [lift, Quotient.lift_spec, Quiver.FreeGroupoid.lift_spec]

Premises used: Quiver.FreeGroupoid.lift_spec, CategoryTheory.Quotient.lift_spec, CategoryTheory.FreeGroupoid.lift
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
E : Type u₂
inst_1 : Groupoid.{v₂, u₂} E
φ : Functor.{v, v₂, u, u₂} C E
X : C
⊢ (lift φ).obj (mk X) = φ.obj X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
E : Type u₂
inst_1 : Groupoid.{v₂, u₂} E
φ : Functor.{v, v₂, u, u₂} C E
X Y : C
f : X ⟶ Y
⊢ (lift φ).map (homMk f) = φ.map f

Tactic:
simpa using Functor.congr_hom (lift_spec φ) f

Premises used: CategoryTheory.Functor.congr_hom, CategoryTheory.FreeGroupoid.lift_spec
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
φ : Functor.{v, v₁, u, u₁} C G
Φ : FreeGroupoid.{v, u} C ⥤ G
hΦ : of C ⋙ Φ = φ
hΦ₁ : Quotient.functor (homRel C) ⋙ Φ = Quiver.FreeGroupoid.lift φ.toPrefunctor
⊢ Φ = lift φ

Tactic:
apply Quotient.lift_unique

Premises used: CategoryTheory.Quotient.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
φ : Functor.{v, v₁, u, u₁} C G
Φ : FreeGroupoid.{v, u} C ⥤ G
hΦ : of C ⋙ Φ = φ
hΦ₁ : Quiver.FreeGroupoid.of C ⋙q (Quotient.functor (homRel C) ⋙ Φ).toPrefunctor = φ.toPrefunctor
⊢ Quotient.functor (homRel C) ⋙ Φ = Quiver.FreeGroupoid.lift φ.toPrefunctor

Tactic:
apply Quiver.FreeGroupoid.lift_unique

Premises used: Quiver.FreeGroupoid.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
φ : Functor.{v, v₁, u, u₁} C G
Φ : FreeGroupoid.{v, u} C ⥤ G
hΦ : of C ⋙ Φ = φ
⊢ Quiver.FreeGroupoid.of C ⋙q (Quotient.functor (homRel C) ⋙ Φ).toPrefunctor = φ.toPrefunctor

Tactic:
congr_arg Functor.toPrefunctor hΦ

Premises used: Prefunctor.comp, congr_arg, CategoryTheory.Functor.toPrefunctor
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
φ : Functor.{v, v₁, u, u₁} C G
Φ : FreeGroupoid.{v, u} C ⥤ G
hΦ : of C ⋙ Φ = φ
⊢ Quiver.FreeGroupoid.of C ⋙q (Quotient.functor (homRel C) ⋙ Φ).toPrefunctor = φ.toPrefunctor

Tactic:
exact congr_arg Functor.toPrefunctor hΦ

Premises used: congr_arg, CategoryTheory.Functor.toPrefunctor
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
rw : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) ((of G ⋙ lift (𝟭 G)) ⋙ of G) (of G)
rw₁ : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (𝟭 G ⋙ of G) (of G)
rw₂ rw₃ : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G) (of G)
⊢ Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G ⋙ lift (𝟭 G) ⋙ of G) (of G)

Tactic:
rw [← Functor.assoc, lift_spec, Functor.id_comp]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.Functor.id_comp, CategoryTheory.FreeGroupoid.lift_spec
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
rw : Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (lift (of G)) (𝟭 (FreeGroupoid.{v₁, u₁} G))
⊢ Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (lift (𝟭 G) ⋙ of G) (𝟭 (FreeGroupoid.{v₁, u₁} G))

Tactic:
rw [lift_unique (of G) (lift (𝟭 G) ⋙ of G) (by rw [← Functor.assoc, lift_spec, Functor.id_comp])]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.FreeGroupoid.lift_unique, CategoryTheory.FreeGroupoid.of, CategoryTheory.FreeGroupoid.lift
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
symm : Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (𝟭 (FreeGroupoid.{v₁, u₁} G)) (lift (of G))
⊢ Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (lift (of G)) (𝟭 (FreeGroupoid.{v₁, u₁} G))

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
hΦ : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G ⋙ 𝟭 (FreeGroupoid.{v₁, u₁} G)) (of G)
⊢ Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (𝟭 (FreeGroupoid.{v₁, u₁} G)) (lift (of G))

Tactic:
apply lift_unique

Premises used: CategoryTheory.FreeGroupoid.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
hΦ hΦ₁ : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G) (of G)
⊢ Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G ⋙ 𝟭 (FreeGroupoid.{v₁, u₁} G)) (of G)

Tactic:
rw [Functor.comp_id]

Premises used: CategoryTheory.Functor.comp_id
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
H : Type u₂
inst_2 : Groupoid.{v₂, u₂} H
φ : Functor.{v, v₁, u, u₁} C G
ψ : Functor.{v₁, v₂, u₁, u₂} G H
symm : lift φ ⋙ ψ = lift (φ ⋙ ψ)
⊢ lift (φ ⋙ ψ) = lift φ ⋙ ψ

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
H : Type u₂
inst_2 : Groupoid.{v₂, u₂} H
φ : Functor.{v, v₁, u, u₁} C G
ψ : Functor.{v₁, v₂, u₁, u₂} G H
hΦ : of C ⋙ lift φ ⋙ ψ = φ ⋙ ψ
⊢ lift φ ⋙ ψ = lift (φ ⋙ ψ)

Tactic:
apply lift_unique

Premises used: CategoryTheory.FreeGroupoid.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
H : Type u₂
inst_2 : Groupoid.{v₂, u₂} H
φ : Functor.{v, v₁, u, u₁} C G
ψ : Functor.{v₁, v₂, u₁, u₂} G H
hΦ : (of C ⋙ lift φ) ⋙ ψ = φ ⋙ ψ
hΦ₁ hΦ₂ : φ ⋙ ψ = φ ⋙ ψ
⊢ of C ⋙ lift φ ⋙ ψ = φ ⋙ ψ

Tactic:
rw [← Functor.assoc, lift_spec]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.FreeGroupoid.lift_spec
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G_1 : Type u₁
inst_1 : Groupoid.{v₁, u₁} G_1
F G : FreeGroupoid.{v, u} C ⥤ G_1
h : of C ⋙ F = of C ⋙ G
rw : lift (of C ⋙ G) = G
rw₁ rw₂ : G = G
⊢ F = G

Tactic:
rw [lift_unique (of C ⋙ G) F h, ← lift_unique (of C ⋙ G) G rfl]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.FreeGroupoid.lift_unique, CategoryTheory.FreeGroupoid.of, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
⊢ Functor.IsLocalization (D := FreeGroupoid.{v, u} C) (of C) ⊤

Tactic:
.mk' _ _ strictUniversalPropertyFixedTarget strictUniversalPropertyFixedTarget

Premises used: CategoryTheory.Functor.IsLocalization.mk', CategoryTheory.FreeGroupoid.strictUniversalPropertyFixedTarget
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
F₁ F₂ : FreeGroupoid.{v, u} C ⥤ G
τ : of C ⋙ F₁ ≅ of C ⋙ F₂
X : C
⊢ (liftNatIso F₁ F₂ τ).hom.app (mk X) = τ.hom.app X

Tactic:
simp [liftNatIso]

Premises used: CategoryTheory.FreeGroupoid.liftNatIso
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u₁
inst_1 : Groupoid.{v₁, u₁} G
F₁ F₂ : FreeGroupoid.{v, u} C ⥤ G
τ : of C ⋙ F₁ ≅ of C ⋙ F₂
X : C
⊢ (liftNatIso F₁ F₂ τ).inv.app (mk X) = τ.inv.app X

Tactic:
simp [liftNatIso]

Premises used: CategoryTheory.FreeGroupoid.liftNatIso
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
⊢ of C ⋙ map F = F ⋙ of D

Tactic:
rfl

Premises used: CategoryTheory.FreeGroupoid, CategoryTheory.Functor.comp, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, Quiver.Path.comp, CategoryTheory.FreeGroupoid.of, rfl