-- Mathlib/CategoryTheory/PathCategory/Basic.lean
theorem lift_unique {C} [Category C] (φ : V ⥤q C) (Φ : Paths V ⥤ C)
    (hΦ : of ⋙q Φ.toPrefunctor = φ) : Φ = lift φ

Proof state:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
Φ : Paths V ⥤ C
hΦ : of ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ

Tactic:
subst_vars

Result:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ Φ = lift (of ⋙q Φ.toPrefunctor)

Proof state:
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil =
    𝟙 (Φ.obj X) ≫
      Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) Quiver.Path.nil ≫ 𝟙 (Φ.obj X)

Tactic:
simp only [Category.comp_id]

Result:
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)

Proof state:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
⊢ Φ.map f = 𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => 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 ⊢
  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]

Result:
no goals

Proof state:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
⊢ Φ.map f = eqToHom ⋯ ≫ (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯

Tactic:
dsimp [lift]

Result:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
⊢ Φ.map f = 𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) f ≫ 𝟙 (Φ.obj Y)

Proof state:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p
⊢ Φ.map (p.cons f') = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) 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')

Result:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p
this : Φ.map (p.cons f') = Φ.map p ≫ Φ.map f'.toPath
⊢ Φ.map (p.cons f') = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p ≫ Φ.map f'.toPath

Proof state:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p
⊢ Φ.map (p.cons f') = Φ.map p ≫ Φ.map f'.toPath

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

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

Tactic:
rintro X

Result:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X : Paths V
⊢ Φ.obj X = (lift (of ⋙q Φ.toPrefunctor)).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
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = 𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p ≫ 𝟙 (Φ.obj b✝)
⊢ Φ.map (p.cons f') =
    𝟙 (Φ.obj X) ≫ Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) (p.cons f') ≫ 𝟙 (Φ.obj c✝)

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

Result:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p
⊢ Φ.map (p.cons f') = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p ≫ Φ.map f'.toPath

Proof state:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    _auto✝

Tactic:
rintro X Y f

Result:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
f : X ⟶ Y
⊢ Φ.map f = eqToHom ⋯ ≫ (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯

Proof state:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p
this : Φ.map (p.cons f') = Φ.map p ≫ Φ.map f'.toPath
⊢ Φ.map (p.cons f') = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp => ihp ≫ Φ.map f.toPath) p ≫ Φ.map f'.toPath

Tactic:
rw [this, ih]

Result:
no goals

Proof state:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ Φ = lift (of ⋙q Φ.toPrefunctor)

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

case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    _auto✝

Proof state:
case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)

Tactic:
apply Functor.map_id

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

Tactic:
rfl

Result:
no goals