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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
nil :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj Y)
    (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)
        (f ≫ Quiver.Path.nil) :
      φ.obj X ⟶ φ.obj Y)
    (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) f :
      φ.obj X ⟶ φ.obj Y)
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj Y)
    (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)
        (f ≫ Quiver.Path.nil) :
      φ.obj X ⟶ φ.obj Y)
    (CategoryStruct.comp (Y := φ.obj Y)
        (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) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
          Quiver.Path.nil) :
      φ.obj X ⟶ φ.obj Y)

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj Y)
    (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)
        (f ≫ Quiver.Path.nil) :
      φ.obj X ⟶ φ.obj Y)
    (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) f :
      φ.obj X ⟶ φ.obj Y)

Tactic:
rfl
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
b c : Paths V
g' : Quiver.Path.{v₁, u₁} Y b
p : b ⟶ c
ih :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj b)
    (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) (f ≫ g') :
      φ.obj X ⟶ φ.obj b)
    (CategoryStruct.comp (Y := φ.obj Y)
        (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) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g') :
      φ.obj X ⟶ φ.obj b)
⊢ f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p

Tactic:
apply Quiver.Path.comp_cons

Premises used: Quiver.Path.comp_cons
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
b c : Paths V
g' : Quiver.Path.{v₁, u₁} Y b
p : b ⟶ c
ih :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj b)
    (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) (f ≫ g') :
      φ.obj X ⟶ φ.obj b)
    (CategoryStruct.comp (Y := φ.obj Y)
        (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) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g') :
      φ.obj X ⟶ φ.obj b)
⊢ f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p

Tactic:
have : f ≫ Quiver.Path.cons g' p = (f ≫ g').cons p := by apply Quiver.Path.comp_cons
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
b c : Paths V
g' : Quiver.Path.{v₁, u₁} Y b
p : b ⟶ c
ih :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj b)
    (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) (f ≫ g') :
      φ.obj X ⟶ φ.obj b)
    (CategoryStruct.comp (Y := φ.obj Y)
        (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) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g') :
      φ.obj X ⟶ φ.obj b)
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
cons :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj c)
    (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)
        (Quiver.Path.cons (f ≫ g') p) :
      φ.obj X ⟶ φ.obj c)
    (CategoryStruct.comp (Y := φ.obj Y)
        (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) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
          (g'.cons p)) :
      φ.obj X ⟶ φ.obj c)
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj c)
    (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)
        (f ≫ g'.cons p) :
      φ.obj X ⟶ φ.obj c)
    (CategoryStruct.comp (Y := φ.obj Y)
        (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) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
          (g'.cons p)) :
      φ.obj X ⟶ φ.obj c)

Tactic:
rw [this]
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
b c : Paths V
g' : Quiver.Path.{v₁, u₁} Y b
p : b ⟶ c
ih :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj b)
    (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) (f ≫ g') :
      φ.obj X ⟶ φ.obj b)
    (CategoryStruct.comp (Y := φ.obj Y)
        (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) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g') :
      φ.obj X ⟶ φ.obj b)
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
cons :
  Eq (α := φ.obj X ⟶ φ.obj c)
    (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) (f ≫ g') ≫
      φ.map p)
    (CategoryStruct.comp (Y := φ.obj Y)
      (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) f)
      (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g' ≫
        φ.map p))
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj c)
    (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)
        (Quiver.Path.cons (f ≫ g') p) :
      φ.obj X ⟶ φ.obj c)
    (CategoryStruct.comp (Y := φ.obj Y)
        (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) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
          (g'.cons p)) :
      φ.obj X ⟶ φ.obj c)

Tactic:
simp only at ih ⊢
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X : V
⊢ (lift φ).map Quiver.Path.nil = 𝟙 (φ.obj X)

Tactic:
rfl

Premises used: rfl
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : V
p : Quiver.Path.{v₁, u₁} X Y
f : Y ⟶ Z
⊢ (lift φ).map (p.cons f) = (lift φ).map p ≫ φ.map f

Tactic:
rfl

Premises used: rfl
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y : V
f : X ⟶ Y
dsimp : 𝟙 (φ.obj X) ≫ φ.map f = φ.map f
⊢ (lift φ).map f.toPath = φ.map f

Tactic:
dsimp [Quiver.Hom.toPath, lift]

Premises used: Quiver.Hom.toPath, CategoryTheory.Paths.lift
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y : V
f : X ⟶ Y
⊢ 𝟙 (φ.obj X) ≫ φ.map f = φ.map f

Tactic:
simp
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
h_obj : ∀ (X : V), (of V ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    (of V ⋙q (lift φ).toPrefunctor).map f =
      Eq.recOn (motive := fun (x : C) (x_1 : φ.obj Y = x) ↦ (of V ⋙q (lift φ).toPrefunctor).obj X ⟶ x) ⋯
        (Eq.recOn (motive := fun (x : C) (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) ⋯ (φ.map f))
⊢ of V ⋙q (lift φ).toPrefunctor = φ

Tactic:
fapply Prefunctor.ext

Premises used: Prefunctor.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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X : V
⊢ (of V ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

Tactic:
rfl
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y : V
f : X ⟶ Y
h_map :
  ∀ (φo : V → C) (φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)),
    (of V ⋙q (lift { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }).toPrefunctor).map f =
      Eq.recOn (motive := fun (x : C) (x_1 : { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj Y = x) ↦
        (of V ⋙q (lift { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }).toPrefunctor).obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : C) (x_1 : { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj X = x) ↦
          x ⟶ { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj Y) ⋯
          ({ obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.map f))
⊢ (of V ⋙q (lift φ).toPrefunctor).map f =
    Eq.recOn (motive := fun (x : C) (x_1 : φ.obj Y = x) ↦ (of V ⋙q (lift φ).toPrefunctor).obj X ⟶ x) ⋯
      (Eq.recOn (motive := fun (x : C) (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) ⋯ (φ.map f))

Tactic:
rcases φ with ⟨φo, φm⟩
-- 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
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
h_map : 𝟙 (φo X) ≫ φm f = φm f
⊢ (of V ⋙q (lift { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }).toPrefunctor).map f =
    Eq.recOn (motive := fun (x : C) (x_1 : { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj Y = x) ↦
      (of V ⋙q (lift { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }).toPrefunctor).obj X ⟶ x) ⋯
      (Eq.recOn (motive := fun (x : C) (x_1 : { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj X = x) ↦
        x ⟶ { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj Y) ⋯
        ({ obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.map f))

Tactic:
dsimp [lift, Quiver.Hom.toPath]

Premises used: Quiver.Hom.toPath, CategoryTheory.Paths.lift
-- 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
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ 𝟙 (φo X) ≫ φm f = φm f

Tactic:
simp
-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
Φ : Paths V ⥤ C
hΦ : of V ⋙q Φ.toPrefunctor = φ
subst_vars : Φ = lift (of V ⋙q Φ.toPrefunctor)
⊢ Φ = lift φ

Tactic:
subst_vars
-- 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
h_obj : ∀ (X : Paths V), Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X
h_map :
  autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
⊢ Φ = lift (of V ⋙q Φ.toPrefunctor)

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
Φ : Paths V ⥤ C
X : Paths V
⊢ Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X

Tactic:
rfl
-- 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 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)
⊢ Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯

Tactic:
dsimp [lift]

Premises used: CategoryTheory.Paths.lift
-- 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
h_map : Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)
⊢ Φ.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)

Tactic:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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
⊢ Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)

Tactic:
apply Functor.map_id

Premises used: CategoryTheory.Functor.map_id
-- 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 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)
h_map :
  ∀
    (ih :
      Φ.map p =
        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),
    Φ.map (p.cons f') =
      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 ≫
        Φ.map f'.toPath
⊢ Φ.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)

Tactic:
simp only [Category.comp_id, Category.id_comp] at ih ⊢

Premises used: CategoryTheory.Category.comp_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
Φ : Paths V ⥤ C
X Y b c : Paths V
p : Quiver.Path.{v₁, u₁} X b
f' : b ⟶ c
ih :
  Φ.map p =
    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
⊢ Φ.map (p ≫ f'.toPath) = Φ.map p ≫ Φ.map f'.toPath

Tactic:
Functor.map_comp Φ p (Quiver.Hom.toPath f')

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
Φ : Paths V ⥤ C
X Y b c : Paths V
p : Quiver.Path.{v₁, u₁} X b
f' : b ⟶ c
ih :
  Φ.map p =
    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
⊢ Φ.map (p.cons f') = Φ.map p ≫ Φ.map f'.toPath

Tactic:
convert! Functor.map_comp Φ p (Quiver.Hom.toPath f')

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
Φ : Paths V ⥤ C
X Y b c : Paths V
p : Quiver.Path.{v₁, u₁} X b
f' : b ⟶ c
ih :
  Φ.map p =
    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
⊢ Φ.map (p.cons f') = Φ.map p ≫ Φ.map f'.toPath

Tactic:
have : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f') := by
        convert! Functor.map_comp Φ p (Quiver.Hom.toPath f')
-- 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 b c : Paths V
p : Quiver.Path.{v₁, u₁} X b
f' : b ⟶ c
ih :
  Φ.map p =
    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
this : Φ.map (p.cons f') = Φ.map p ≫ Φ.map f'.toPath
h_map :
  Φ.map p ≫ Φ.map f'.toPath =
    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 ≫
      Φ.map f'.toPath
h_map₁ h_map₂ :
  Eq (α := Φ.obj X ⟶ Φ.obj c)
    (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 ≫
      Φ.map f'.toPath)
    (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 ≫
      Φ.map f'.toPath)
⊢ Φ.map (p.cons f') =
    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 ≫
      Φ.map f'.toPath

Tactic:
rw [this, ih]