-- 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
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
g : Y ⟶ Z
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)
    (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)
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj Z)
    (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 Z)
    (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 Z)
have cons : ∀ {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)),
  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: induction g with
    | nil =>
      rw [Category.comp_id]
      rfl
    | cons g' p ih =>
      have : f ≫ Quiver.Path.cons g' p = (f ≫ g').cons p := by apply Quiver.Path.comp_cons
      rw [this]
      simp only at ih ⊢
      rw [ih, Category.assoc]
Cleared hypotheses: g