awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯
have 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)
Tactic: dsimp [lift]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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) ≫
      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)
have h_map : Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)
Tactic: simp only [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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)
⊢ Φ.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)
have 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
Tactic: simp only [Category.comp_id, Category.id_comp] at ih ⊢
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (hypothesis)
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') =
    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
have this : Φ.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')
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ Φ.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
have 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
Tactic: rw [this, ih]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ Φ.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
have 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)
Tactic: rw [this, ih]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ Φ.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)
have 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)
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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)
⊢ Φ.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)
have 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)
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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 ⋯
⊢ F = G
have h_obj₁ : ∀ (X : Paths V), F.obj X = G.obj X
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ F = G
have h_map : autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom sorry ≫ G.map f ≫ eqToHom sorry) Functor.ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ F.obj X = G.obj X
have h_obj₁ : G.obj X = G.obj X
Tactic: rw [h_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ 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 ⋯))
have h_map : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X))
  (CategoryStruct.comp (Y := G.obj X) (eqToHom sorry) (G.map Quiver.Path.nil ≫ eqToHom sorry))
Tactic: erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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 ⋯))
⊢ 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 ⋯))
have h_map₁ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (eqToHom sorry ≫ 𝟙 (G.obj X) ≫ eqToHom sorry)
Tactic: erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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 ⋯)
⊢ 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 ⋯))
have h_map₂ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (CategoryStruct.comp (Y := G.obj X) (eqToHom sorry) (eqToHom sorry))
Tactic: erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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 ⋯))
⊢ 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 ⋯))
have h_map₃ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (eqToHom sorry)
Tactic: erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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 ⋯)
⊢ 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 ⋯))
have h_map₄ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
Tactic: erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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 ⋯
⊢ F.map (g.cons e) = eqToHom ⋯ ≫ G.map (g.cons e) ≫ eqToHom ⋯
have h_map : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj c)
  ((eqToHom sorry ≫ G.map g ≫ eqToHom sorry) ≫ eqToHom sorry ≫ G.map e.toPath ≫ eqToHom sorry : F.obj X ⟶ F.obj c)
  (eqToHom sorry ≫ (G.map g ≫ G.map e.toPath) ≫ eqToHom sorry : F.obj X ⟶ F.obj c)
Tactic: erw [F.map_comp g (Quiver.Hom.toPath e), G.map_comp g (Quiver.Hom.toPath e), ih, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have h_map : Eq (α := F.obj X ⟶ F.obj X) (F.map Quiver.Path.nil)
  (CategoryStruct.comp (Y := G.obj X) (eqToHom sorry) (G.map Quiver.Path.nil ≫ eqToHom sorry))
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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 ⋯))
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
have h_map₁ : ∀ {b c : Paths V} (g : Quiver.Path.{v₁, u₁} X b) (e : b ⟶ c) (ih : F.map g = eqToHom sorry ≫ G.map g ≫ eqToHom sorry),
  F.map (g.cons e) = eqToHom sorry ≫ G.map (g.cons e) ≫ eqToHom sorry
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ composePath (f.comp g) = composePath f ≫ composePath g
have nil : composePath (f.comp Path.nil) = composePath f ≫ composePath Path.nil
Tactic: induction g with
  | nil => simp
  | cons g e ih => simp [ih]
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
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
⊢ composePath (f.comp g) = composePath f ≫ composePath g
have 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)
Tactic: induction g with
  | nil => simp
  | cons g e ih => simp [ih]
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Quotient (pathsHomRel C)
⊢ Functor.obj (𝟭 (Quotient (pathsHomRel C))) X ≅ Functor.obj (quotientPathsTo C ⋙ toQuotientPaths C) X
have 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))
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
as : Paths C
⊢ 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))
have 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) sorry)
  (𝟙 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
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)
⊢ P = ⊤
have h : ∀ ⦃X Y : Paths V⦄ (f : X ⟶ Y), P f ↔ ⊤ f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
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
have h : P f → ⊤ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
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
⊢ P f ↔ ⊤ f
have h₁ : ⊤ f → P f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
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)
⊢ P = ⊤
have h : ∀ ⦃X Y : Paths V⦄ (f : X ⟶ Y), P f ↔ ⊤ f
Tactic: ext