awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
h_map :
  Φ.map Quiver.Path.nil =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ Φ.obj X ⟶ Φ.obj Y) (𝟙 (Φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : Φ.obj X ⟶ Φ.obj b) ↦ ihp ≫ Φ.map f.toPath)
          Quiver.Path.nil ≫
        𝟙 (Φ.obj X)
h_map₁ :
  ∀ {b c : Paths V} (p : Quiver.Path.{v₁, u₁} X b) (f' : b ⟶ c)
    (ih :
      Φ.map p =
        𝟙 (Φ.obj X) ≫
          Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ Φ.obj X ⟶ Φ.obj Y) (𝟙 (Φ.obj X))
              (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : Φ.obj X ⟶ Φ.obj b) ↦
                ihp ≫ Φ.map f.toPath)
              p ≫
            𝟙 (Φ.obj b)),
    Φ.map (p.cons f') =
      𝟙 (Φ.obj X) ≫
        Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ Φ.obj X ⟶ Φ.obj Y) (𝟙 (Φ.obj X))
            (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : Φ.obj X ⟶ Φ.obj b) ↦ ihp ≫ Φ.map f.toPath)
            (p.cons f') ≫
          𝟙 (Φ.obj c)
⊢ Φ.map f =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ Φ.obj X ⟶ Φ.obj Y) (𝟙 (Φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : Φ.obj X ⟶ Φ.obj b) ↦ ihp ≫ Φ.map f.toPath)
          f ≫
        𝟙 (Φ.obj Y)

Tactic:
induction f with
    | nil =>
      simp only [Category.comp_id]
      apply Functor.map_id
    | cons p f' ih =>
      simp only [Category.comp_id, Category.id_comp] at ih ⊢
      -- Porting note: Had to do substitute `p.cons f'` and `f'.toPath` by their fully qualified
      -- versions in this `have` clause (elsewhere too).
      have : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f') := by
        convert! Functor.map_comp Φ p (Quiver.Hom.toPath f')
      rw [this, ih]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
h_obj₁ : ∀ (X : Paths V), F.obj X = G.obj X
h_map : autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) Functor.ext._auto_1
⊢ F = G

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X : Paths V
h_obj₁ h_obj₂ : G.obj X = G.obj X
⊢ F.obj X = G.obj X

Tactic:
rw [h_obj]
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y : Paths V
h_map :
  Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X))
    (CategoryStruct.comp (Y := G.obj X) (eqToHom ⋯) (G.map Quiver.Path.nil ≫ eqToHom ⋯))
h_map₁ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (eqToHom ⋯ ≫ 𝟙 (G.obj X) ≫ eqToHom ⋯)
h_map₂ :
  Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (CategoryStruct.comp (Y := G.obj X) (eqToHom ⋯) (eqToHom ⋯))
h_map₃ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (eqToHom ⋯)
h_map₄ h_map₅ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
⊢ Eq (α := F.obj X ⟶ F.obj X) (F.map Quiver.Path.nil)
    (CategoryStruct.comp (Y := G.obj X) (eqToHom ⋯) (G.map Quiver.Path.nil ≫ eqToHom ⋯))

Tactic:
erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Functor.map_id, CategoryTheory.eqToHom_trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y b c : Paths V
g : Quiver.Path.{v₁, u₁} X b
e : b ⟶ c
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
h_map :
  Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj c)
    ((eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯ : F.obj X ⟶ F.obj c)
    (eqToHom ⋯ ≫ (G.map g ≫ G.map e.toPath) ≫ eqToHom ⋯ : F.obj X ⟶ F.obj c)
⊢ F.map (g.cons e) = eqToHom ⋯ ≫ G.map (g.cons e) ≫ eqToHom ⋯

Tactic:
erw [F.map_comp g (Quiver.Hom.toPath e), G.map_comp g (Quiver.Hom.toPath e), ih, h]

Premises used: Quiver.Hom.toPath, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y b c : Paths V
g : Quiver.Path.{v₁, u₁} X b
e : b ⟶ c
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj c)
    ((eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯ : F.obj X ⟶ F.obj c)
    (eqToHom ⋯ ≫ (G.map g ≫ G.map e.toPath) ≫ eqToHom ⋯ : F.obj X ⟶ F.obj c)

Tactic:
simp only [Category.id_comp, eqToHom_refl, eqToHom_trans_assoc, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y : Paths V
f : X ⟶ Y
h_map :
  Eq (α := F.obj X ⟶ F.obj X) (F.map Quiver.Path.nil)
    (CategoryStruct.comp (Y := G.obj X) (eqToHom ⋯) (G.map Quiver.Path.nil ≫ eqToHom ⋯))
h_map₁ :
  ∀ {b c : Paths V} (g : Quiver.Path.{v₁, u₁} X b) (e : b ⟶ c) (ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯),
    F.map (g.cons e) = eqToHom ⋯ ≫ G.map (g.cons e) ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
induction f with
    | nil => erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
    | cons g e ih =>
      erw [F.map_comp g (Quiver.Hom.toPath e), G.map_comp g (Quiver.Hom.toPath e), ih, h]
      simp only [Category.id_comp, eqToHom_refl, eqToHom_trans_assoc, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_refl, CategoryTheory.Functor.map_id, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.eqToHom_trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
X Y Z : Paths V
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.mapPath (f ≫ g) = (F.mapPath f).comp (F.mapPath g)

Tactic:
Prefunctor.mapPath_comp _ _ _

Premises used: Prefunctor.mapPath_comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := X ⟶ X) (composePath Path.nil) (𝟙 X)

Tactic:
rfl

Premises used: CategoryTheory.composePath, rfl
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
p : Path.{v₁, u₁} X Y
e : Y ⟶ Z
⊢ composePath (p.cons e) = composePath p ≫ e

Tactic:
rfl

Premises used: CategoryTheory.composePath, rfl
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ composePath f.toPath = f

Tactic:
Category.id_comp _

Premises used: CategoryTheory.composePath, Quiver.Hom.toPath, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Path.{v₁, u₁} X Y
⊢ composePath (f.comp Path.nil) = composePath f ≫ composePath Path.nil

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Path.{v₁, u₁} X Y
b c : C
g : Path.{v₁, u₁} Y b
e : b ⟶ c
ih : composePath (f.comp g) = composePath f ≫ composePath g
⊢ composePath (f.comp (g.cons e)) = composePath f ≫ composePath (g.cons e)

Tactic:
simp [ih]
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Path.{v₁, u₁} X Y
g : Path.{v₁, u₁} Y Z
nil : composePath (f.comp Path.nil) = composePath f ≫ composePath Path.nil
cons :
  ∀ {b c : C} (g : Path.{v₁, u₁} Y b) (e : b ⟶ c) (ih : composePath (f.comp g) = composePath f ≫ composePath g),
    composePath (f.comp (g.cons e)) = composePath f ≫ composePath (g.cons e)
⊢ composePath (f.comp g) = composePath f ≫ composePath g

Tactic:
induction g with
  | nil => simp
  | cons g e ih => simp [ih]
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Paths C
⊢ Eq.{v₁ + 1} (α := X ⟶ X) (composePath (𝟙 X))
    (𝟙
      (have this := X;
      this))

Tactic:
rfl

Premises used: CategoryTheory.composePath, rfl
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Paths C
f : X ⟶ Y
g : Y ⟶ Z
⊢ composePath (f ≫ g) = composePath f ≫ composePath g

Tactic:
composePath_comp f g

Premises used: CategoryTheory.composePath_comp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ pathsHomRel.{v₁, u₁} C (Hom.toPath (𝟙 X)) (𝟙 (Quotient.as (r := pathsHomRel C) (Quotient.mk (r := pathsHomRel C) X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ pathsHomRel C (f ≫ g).toPath (f.toPath ≫ g.toPath)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
mk :
  (as : Paths C) →
    Iso (C := Quotient (pathsHomRel C))
      (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as))
      (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as))
⊢ Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅ Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
as : Paths C
⊢ Iso (C := Quotient (pathsHomRel C)) (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as))
    (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Quotient (pathsHomRel C)
f : X.as (r := pathsHomRel C) ⟶ Y.as (r := pathsHomRel C)
⊢ pathsHomRel C
    (f ≫
      𝟙
        (Quotient.as (r := pathsHomRel C)
          (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) (Y.as (r := pathsHomRel C))))))
    (𝟙
        (Quotient.as (r := pathsHomRel C)
          (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) (X.as (r := pathsHomRel C))))) ≫
      Hom.toPath (Functor.map (quotientPathsTo C) (Quot.mk (HomRel.CompClosure (pathsHomRel C)) f)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Quotient (pathsHomRel C)
f : X.as (r := pathsHomRel C) ⟶ Y.as (r := pathsHomRel C)
⊢ Eq (α := Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ⟶ Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) Y)
    (CategoryStruct.comp (Y := Functor.obj (𝟭 (Quotient (pathsHomRel C))) Y)
      (Functor.map (𝟭 (Quotient (pathsHomRel C))) (Quot.mk (HomRel.CompClosure (pathsHomRel C)) f))
      (Iso.hom
        ((fun (X : Quotient (pathsHomRel C)) ↦
            (Quotient.casesOn (r := pathsHomRel C) (motive := fun (t : Quotient (pathsHomRel C)) ↦
                (h : X = t) →
                  Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅ Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                X
                (fun (as : Paths C) (h : X = Quotient.mk (r := pathsHomRel C) as) ↦
                  Eq.ndrec (motive := fun (X : Quotient (pathsHomRel C)) ↦
                    Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅
                      Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                    (Iso.refl (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as))) ⋯)
                ⋯ :
              Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅ Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X))
          Y)))
    (Iso.hom
        ((fun (X : Quotient (pathsHomRel C)) ↦
            (Quotient.casesOn (r := pathsHomRel C) (motive := fun (t : Quotient (pathsHomRel C)) ↦
                (h : X = t) →
                  Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅ Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                X
                (fun (as : Paths C) (h : X = Quotient.mk (r := pathsHomRel C) as) ↦
                  Eq.ndrec (motive := fun (X : Quotient (pathsHomRel C)) ↦
                    Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅
                      Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                    (Iso.refl (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as))) ⋯)
                ⋯ :
              Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅ Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X))
          X) ≫
      Functor.map (quotientPathsTo C ⋙ toQuotientPaths C) (Quot.mk (HomRel.CompClosure (pathsHomRel C)) f))

Tactic:
exact Quot.sound (HomRel.CompClosure.of (by simp))

Premises used: Quot.sound, CategoryTheory.HomRel.CompClosure.of
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y)
    (Functor.map (toQuotientPaths C ⋙ quotientPathsTo C) f ≫
      Iso.hom
        ((fun (x : C) ↦
            (Iso.refl (Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x) :
              Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x ≅
                Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x))
          Y))
    (Iso.hom
        ((fun (x : C) ↦
            (Iso.refl (Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x) :
              Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x ≅
                Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x))
          X) ≫
      Functor.map (𝟭 C) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
as : Paths C
mk :
  Eq.{v₁ + 1} (α := as ⟶ as)
    (Quot.liftOn (r := HomRel.CompClosure (pathsHomRel C)) (𝟙 (Quotient.mk (r := pathsHomRel C) as))
      (fun (f : as ⟶ as) ↦ composePath f) ⋯)
    (𝟙 as)
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as) ⟶
      Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))
    (CategoryStruct.comp (Y :=
        Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C)
          (Functor.obj (toQuotientPaths C)
            (Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))))
        (Functor.map (quotientPathsTo C)
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : Quotient (pathsHomRel C)) ↦
                  Quotient.casesOn (r := pathsHomRel C) (motive := fun (t : Quotient (pathsHomRel C)) ↦
                    (h : X = t) →
                      Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅
                        Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                    X
                    (fun (as : Paths C) (h : X = Quotient.mk (r := pathsHomRel C) as) ↦
                      Eq.ndrec (motive := fun (X : Quotient (pathsHomRel C)) ↦
                        Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅
                          Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X)
                        (Iso.refl (Functor.obj (𝟭 (Quotient (pathsHomRel C))) (Quotient.mk (r := pathsHomRel C) as))) ⋯)
                    ⋯)
                ⋯))
            (Quotient.mk (r := pathsHomRel C) as)))
        (NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (x : C) ↦ Iso.refl (Functor.obj.{v₁, v₁, u₁, u₁} (toQuotientPaths C ⋙ quotientPathsTo C) x)) ⋯))
          (Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))) :
      Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as) ⟶
        Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))
    (𝟙 (Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as)) :
      Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as) ⟶
        Functor.obj (C := Quotient (pathsHomRel C)) (quotientPathsTo C) (Quotient.mk (r := pathsHomRel C) as))

Tactic:
simp only [Functor.id_obj,
               quotientPathsTo_obj, Functor.comp_obj, toQuotientPaths_obj_as,
               NatIso.ofComponents_hom_app, Iso.refl_hom, quotientPathsTo_map, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.quotientPathsTo_obj, CategoryTheory.Category.comp_id, CategoryTheory.Functor.id_obj, CategoryTheory.toQuotientPaths_obj_as, CategoryTheory.Iso.refl_hom, CategoryTheory.quotientPathsTo_map, CategoryTheory.NatIso.ofComponents_hom_app
-- Module: Mathlib.CategoryTheory.PathCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
as : Paths C
⊢ Eq.{v₁ + 1} (α := as ⟶ as)
    (Quot.liftOn (r := HomRel.CompClosure (pathsHomRel C)) (𝟙 (Quotient.mk (r := pathsHomRel C) as))
      (fun (f : as ⟶ as) ↦ composePath f) ⋯)
    (𝟙 as)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : Prefunctor.obj (of V) u ⟶ Prefunctor.obj (of V) v) (q : v ⟶ w),
    P p → P (p ≫ Prefunctor.map (of V) q)
h : ∀ ⦃X Y : Paths V⦄ (f : X ⟶ Y), P f ↔ ⊤ f
⊢ P = ⊤

Tactic:
ext
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : Prefunctor.obj (of V) u ⟶ Prefunctor.obj (of V) v) (q : v ⟶ w),
    P p → P (p ≫ Prefunctor.map (of V) q)
X Y : Paths V
f : X ⟶ Y
h : P f → ⊤ f
h₁ : ⊤ f → P f
⊢ P f ↔ ⊤ f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : Prefunctor.obj (of V) u ⟶ Prefunctor.obj (of V) v) (q : v ⟶ w),
    P p → P (p ≫ Prefunctor.map (of V) q)
X Y : Paths V
f : X ⟶ Y
⊢ P f → ⊤ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : Prefunctor.obj (of V) u ⟶ Prefunctor.obj (of V) v) (q : v ⟶ w),
    P p → P (p ≫ Prefunctor.map (of V) q)
X Y : Paths V
f : X ⟶ Y
⊢ ⊤ f → P f

Tactic:
fun _ ↦ induction (fun f ↦ P f) id comp _

Premises used: CategoryTheory.Paths.induction
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : Prefunctor.obj (of V) u ⟶ Prefunctor.obj (of V) v) (q : v ⟶ w),
    P p → P (p ≫ Prefunctor.map (of V) q)
X Y : Paths V
f : X ⟶ Y
⊢ ⊤ f → P f

Tactic:
exact fun _ ↦ induction (fun f ↦ P f) id comp _

Premises used: CategoryTheory.Paths.induction
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
h : ∀ ⦃X Y : Paths V⦄ (f : X ⟶ Y), P f ↔ ⊤ f
⊢ P = ⊤

Tactic:
ext
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
X Y : Paths V
f : X ⟶ Y
h : P f → ⊤ f
h₁ : ⊤ f → P f
⊢ P f ↔ ⊤ f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
X Y : Paths V
f : X ⟶ Y
⊢ P f → ⊤ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
X Y : Paths V
f : X ⟶ Y
⊢ ⊤ f → P f

Tactic:
fun _ ↦ induction' (fun f ↦ P f) id comp _

Premises used: CategoryTheory.Paths.induction'
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
X Y : Paths V
f : X ⟶ Y
⊢ ⊤ f → P f

Tactic:
exact fun _ ↦ induction' (fun f ↦ P f) id comp _

Premises used: CategoryTheory.Paths.induction'
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
inst_1 : P.IsMultiplicative
hP : ∀ {u v : V} (p : u ⟶ v), P (X := Prefunctor.obj (of V) u) (Prefunctor.map (of V) p)
⊢ P = ⊤

Tactic:
morphismProperty_eq_top _ _ (P.id_mem _) (fun _ q hp ↦ P.comp_mem _ _ hp (hP q))

Premises used: CategoryTheory.MorphismProperty.comp_mem, Prefunctor.map, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.Paths.of, CategoryTheory.Paths.morphismProperty_eq_top, Prefunctor.obj
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
V : Type u₁
inst_1 : Quiver.{v₁, u₁} V
F G : Paths V ⥤ C
α_app : (v : V) → F.obj v ⟶ G.obj v
α_nat : ∀ {X Y : V} (f : X ⟶ Y), F.map f.toPath ≫ α_app Y = α_app X ≫ G.map f.toPath
apply : MorphismProperty.naturalityProperty α_app = ⊤
⊢ ∀ ⦃X Y : Paths V⦄ (f : X ⟶ Y), F.map f ≫ α_app Y = α_app X ≫ G.map f

Tactic:
apply MorphismProperty.of_eq_top
      (P := MorphismProperty.naturalityProperty (F₁ := F) α_app)

Premises used: CategoryTheory.MorphismProperty.of_eq_top
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
V : Type u₁
inst_1 : Quiver.{v₁, u₁} V
F G : Paths V ⥤ C
α_app : (v : V) → F.obj v ⟶ G.obj v
α_nat : ∀ {X Y : V} (f : X ⟶ Y), F.map f.toPath ≫ α_app Y = α_app X ≫ G.map f.toPath
⊢ MorphismProperty.naturalityProperty α_app = ⊤

Tactic:
morphismProperty_eq_top_of_isMultiplicative _ _ α_nat

Premises used: CategoryTheory.Paths.morphismProperty_eq_top_of_isMultiplicative