-- 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
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)
    (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)
    (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 (α := φ.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))
have cons₁ : Eq (α := φ.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' ≫
      φ.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))
Tactic: rw [ih, Category.assoc]