awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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 φ = φ
⊢ Symmetrify.of ⋙q
      (Paths.of (Symmetrify V) ⋙q
        (Quotient.functor redStep ⋙
            CategoryTheory.Quotient.lift redStep (Paths.lift (Symmetrify.lift φ)) ⋯).toPrefunctor) =
    φ
have rw₂ : φ = φ
Tactic: rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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 = φ
⊢ Φ = lift φ
have hΦ₁ : Quotient.functor redStep ⋙ Φ = Paths.lift (Symmetrify.lift φ)
Tactic: apply Quotient.lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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 = φ
⊢ Quotient.functor redStep ⋙ Φ = Paths.lift (Symmetrify.lift φ)
have hΦ₁ : Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor = Symmetrify.lift φ
Tactic: apply Paths.lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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 = φ
⊢ Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor = Symmetrify.lift φ
have fapply : Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor) = φ
Tactic: fapply @Quiver.Symmetrify.lift_unique _ _ _ _ _ _ _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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) = φ
⊢ Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor = Symmetrify.lift φ
have 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)
Tactic: fapply @Quiver.Symmetrify.lift_unique _ _ _ _ _ _ _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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 (Quotient.functor redStep ⋙ Φ).toPrefunctor) = φ
have rw : Symmetrify.of ⋙q (Paths.of (Symmetrify V) ⋙q (Functor.toPrefunctor (Quotient.functor redStep) ⋙q Φ.toPrefunctor)) = φ
Tactic: rw [← Functor.toPrefunctor_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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
⊢ (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (reverse f) =
    reverse ((Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)
have 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)))
Tactic: simp only [← Functor.toPrefunctor_comp, Prefunctor.comp_map, Paths.of_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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 (α :=
    (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)))
have 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)))
Tactic: change Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
      Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (hypothesis)
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 (Groupoid.inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (Groupoid.inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
have 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)))
Tactic: have := Functor.map_inv Φ ((Quotient.functor redStep).toPrefunctor.map f.toPath)
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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 (Groupoid.inv (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
    (Groupoid.inv (Φ.map (Prefunctor.map (Functor.toPrefunctor (Quotient.functor redStep)) f.toPath)))
have 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))
Tactic: convert! this
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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))
⊢ 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)))
have 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)))
Tactic: convert! this
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
Goal:
V : Type u
inst : Quiver.{v, u} V
⊢ Eq (α := Quiver.FreeGroupoid.{u, v} V ⥤ Quiver.FreeGroupoid.{u, v} V) (lift (𝟭q V ⋙q of V))
    (𝟭 (Quiver.FreeGroupoid.{u, v} V))
have symm : Eq (α := Quiver.FreeGroupoid.{u, v} V ⥤ Quiver.FreeGroupoid.{u, v} V) (𝟭 (Quiver.FreeGroupoid.{u, v} V))
  (lift (𝟭q V ⋙q of V))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
Goal:
V : Type u
inst : Quiver.{v, u} V
⊢ Eq (α := Quiver.FreeGroupoid.{u, v} V ⥤ Quiver.FreeGroupoid.{u, v} V) (𝟭 (Quiver.FreeGroupoid.{u, v} V))
    (lift (𝟭q V ⋙q of V))
have hΦ : Eq (α := V ⥤q Quiver.FreeGroupoid.{u, v} V) (of V ⋙q Functor.toPrefunctor (𝟭 (Quiver.FreeGroupoid.{u, v} V)))
  (𝟭q V ⋙q of V)
Tactic: apply lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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''
⊢ lift (φ ⋙q φ' ⋙q of V'') = lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')
have symm : lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoid (goal)
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''
⊢ lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')
have hΦ : of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''
Tactic: apply lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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)
⊢ x = x_1
have refl : x = x
Tactic: cases h
Cleared hypotheses: x_1, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (hypothesis)
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
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map f = (Quiver.FreeGroupoid.lift φ.toPrefunctor).map g
have this : ∀ {X Y : C} (f : X ⟶ Y),
  Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) sorry sorry =
    φ.toPrefunctor.map f
Tactic: have {X Y : C} (f : X ⟶ Y) :=
        Prefunctor.congr_hom (Quiver.FreeGroupoid.lift_spec φ.toPrefunctor) f
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map f = (Quiver.FreeGroupoid.lift φ.toPrefunctor).map g
have 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)))
Tactic: induction r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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)))
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map f = (Quiver.FreeGroupoid.lift φ.toPrefunctor).map g
have 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))
Tactic: induction r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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
⊢ (of C ⋙ lift φ).toPrefunctor = φ.toPrefunctor
have change : Quiver.FreeGroupoid.of C ⋙q Functor.toPrefunctor (Quotient.functor (homRel C)) ⋙q (lift φ).toPrefunctor = φ.toPrefunctor
Tactic: change Quiver.FreeGroupoid.of C ⋙q
      (Quotient.functor (FreeGroupoid.homRel C)).toPrefunctor ⋙q
        (lift φ).toPrefunctor = φ.toPrefunctor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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 ⋙ Φ = φ
⊢ Φ = lift φ
have hΦ₁ : Quotient.functor (homRel C) ⋙ Φ = Quiver.FreeGroupoid.lift φ.toPrefunctor
Tactic: apply Quotient.lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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 ⋙ Φ = φ
⊢ Quotient.functor (homRel C) ⋙ Φ = Quiver.FreeGroupoid.lift φ.toPrefunctor
have hΦ₁ : Quiver.FreeGroupoid.of C ⋙q (Quotient.functor (homRel C) ⋙ Φ).toPrefunctor = φ.toPrefunctor
Tactic: apply Quiver.FreeGroupoid.lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
⊢ Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G ⋙ lift (𝟭 G) ⋙ of G) (of G)
have rw : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) ((of G ⋙ lift (𝟭 G)) ⋙ of G) (of G)
Tactic: rw [← Functor.assoc, lift_spec, Functor.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
rw : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) ((of G ⋙ lift (𝟭 G)) ⋙ of G) (of G)
⊢ Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G ⋙ lift (𝟭 G) ⋙ of G) (of G)
have rw₁ : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (𝟭 G ⋙ of G) (of G)
Tactic: rw [← Functor.assoc, lift_spec, Functor.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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)
⊢ Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G ⋙ lift (𝟭 G) ⋙ of G) (of G)
have rw₂ : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G) (of G)
Tactic: rw [← Functor.assoc, lift_spec, Functor.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
⊢ Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (lift (𝟭 G) ⋙ of G) (𝟭 (FreeGroupoid.{v₁, u₁} G))
have rw : Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (lift (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])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
⊢ Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (lift (of G)) (𝟭 (FreeGroupoid.{v₁, u₁} G))
have symm : Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (𝟭 (FreeGroupoid.{v₁, u₁} G)) (lift (of G))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
⊢ Eq (α := FreeGroupoid.{v₁, u₁} G ⥤ FreeGroupoid.{v₁, u₁} G) (𝟭 (FreeGroupoid.{v₁, u₁} G)) (lift (of G))
have hΦ : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G ⋙ 𝟭 (FreeGroupoid.{v₁, u₁} G)) (of G)
Tactic: apply lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
G : Type u₁
inst : Groupoid.{v₁, u₁} G
⊢ Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G ⋙ 𝟭 (FreeGroupoid.{v₁, u₁} G)) (of G)
have hΦ : Eq (α := G ⥤ FreeGroupoid.{v₁, u₁} G) (of G) (of G)
Tactic: rw [Functor.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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
⊢ lift (φ ⋙ ψ) = lift φ ⋙ ψ
have symm : lift φ ⋙ ψ = lift (φ ⋙ ψ)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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
⊢ lift φ ⋙ ψ = lift (φ ⋙ ψ)
have hΦ : of C ⋙ lift φ ⋙ ψ = φ ⋙ ψ
Tactic: apply lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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
⊢ of C ⋙ lift φ ⋙ ψ = φ ⋙ ψ
have hΦ : (of C ⋙ lift φ) ⋙ ψ = φ ⋙ ψ
Tactic: rw [← Functor.assoc, lift_spec]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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 φ) ⋙ ψ = φ ⋙ ψ
⊢ of C ⋙ lift φ ⋙ ψ = φ ⋙ ψ
have hΦ₁ : φ ⋙ ψ = φ ⋙ ψ
Tactic: rw [← Functor.assoc, lift_spec]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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
⊢ F = G
have rw : lift (of C ⋙ G) = G
Tactic: rw [lift_unique (of C ⋙ G) F h, ← lift_unique (of C ⋙ G) G rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
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
⊢ F = G
have rw₁ : G = G
Tactic: rw [lift_unique (of C ⋙ G) F h, ← lift_unique (of C ⋙ G) G rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := FreeGroupoid.{v, u} C ⥤ FreeGroupoid.{v, u} C) (map (𝟭 C)) (𝟭 (FreeGroupoid.{v, u} C))
have symm : Eq (α := FreeGroupoid.{v, u} C ⥤ FreeGroupoid.{v, u} C) (𝟭 (FreeGroupoid.{v, u} C)) (map (𝟭 C))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := FreeGroupoid.{v, u} C ⥤ FreeGroupoid.{v, u} C) (𝟭 (FreeGroupoid.{v, u} C)) (map (𝟭 C))
have hΦ : Eq (α := C ⥤ FreeGroupoid.{v, u} C) (of C ⋙ 𝟭 (FreeGroupoid.{v, u} C)) (𝟭 C ⋙ of C)
Tactic: apply lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Category.{v₂, u₂} E
φ : Functor.{v, v₁, u, u₁} C D
φ' : Functor.{v₁, v₂, u₁, u₂} D E
⊢ map (φ ⋙ φ') = map φ ⋙ map φ'
have symm : map φ ⋙ map φ' = map (φ ⋙ φ')
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Category.{v₂, u₂} E
φ : Functor.{v, v₁, u, u₁} C D
φ' : Functor.{v₁, v₂, u₁, u₂} D E
⊢ map φ ⋙ map φ' = map (φ ⋙ φ')
have hΦ : of C ⋙ map φ ⋙ map φ' = (φ ⋙ φ') ⋙ of E
Tactic: apply lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
⊢ map F ⋙ lift G = lift (F ⋙ G)
have hΦ : of C ⋙ map F ⋙ lift G = F ⋙ G
Tactic: apply lift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
⊢ of C ⋙ map F ⋙ lift G = F ⋙ G
have hΦ : (of C ⋙ map F) ⋙ lift G = F ⋙ G
Tactic: rw [← Functor.assoc, of_comp_map, Functor.assoc, lift_spec G]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
hΦ : (of C ⋙ map F) ⋙ lift G = F ⋙ G
⊢ of C ⋙ map F ⋙ lift G = F ⋙ G
have hΦ₁ : (F ⋙ of D) ⋙ lift G = F ⋙ G
Tactic: rw [← Functor.assoc, of_comp_map, Functor.assoc, lift_spec G]