-- Mathlib/CategoryTheory/PathCategory/Basic.lean
theorem ext_functor {C} [Category C] {F G : Paths V ⥤ C} (h_obj : F.obj = G.obj)
    (h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath =
        eqToHom (congr_fun h_obj a) ≫ G.map e.toPath ≫ eqToHom (congr_fun h_obj.symm b)) :
    F = G

Proof state:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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

Tactic:
rw [h_obj]

Result:
no goals

Proof state:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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 Y' Z' : Paths V
g : Quiver.Path X Y'
e : Y' ⟶ Z'
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ (eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (G.map g ≫ G.map e.toPath) ≫ eqToHom ⋯

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

Result:
no goals

Proof state:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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

Tactic:
fapply Functor.ext

Result:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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

case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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 ⋯
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) _auto✝

Proof state:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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 ⋯
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) _auto✝

Tactic:
intro X Y f

Result:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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 ⋯

Proof state:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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 ⋯

Tactic:
induction' f with Y' Z' g e ih

Result:
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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.map Quiver.Path.nil = eqToHom ⋯ ≫ G.map Quiver.Path.nil ≫ eqToHom ⋯

case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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 Y' Z' : Paths V
g : Quiver.Path X Y'
e : Y' ⟶ Z'
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ F.map (g.cons e) = eqToHom ⋯ ≫ G.map (g.cons e) ≫ eqToHom ⋯

Proof state:
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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.map Quiver.Path.nil = eqToHom ⋯ ≫ G.map Quiver.Path.nil ≫ eqToHom ⋯

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

Result:
no goals

Proof state:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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

Tactic:
intro X

Result:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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

Proof state:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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 Y' Z' : Paths V
g : Quiver.Path X Y'
e : Y' ⟶ Z'
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ 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]

Result:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, 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 Y' Z' : Paths V
g : Quiver.Path X Y'
e : Y' ⟶ Z'
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ (eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (G.map g ≫ G.map e.toPath) ≫ eqToHom ⋯