-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
X Y Z_1 : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
f : X ⟶ Y
g : Y ⟶ Z_1
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_3, v_1, u_3, u_1} J C)
      { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
        map := fun {X_1 Y : J} (φ : X_1 ⟶ Y) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (X.left.map φ) (X.right.map φ) ⋯),
        map_id := ⋯, map_comp := ⋯ }
      { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
        map := fun {X Y : J} (φ : X ⟶ Y) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Z_1.left.map φ) (Z_1.right.map φ) ⋯),
        map_id := ⋯, map_comp := ⋯ })
    {
      app := fun (j : J) ↦
        data.mapZ (W₁ := W₁) (W₂ := W₂)
          (Arrow.homMk ((Arrow.Hom.left (f ≫ g)).app j) ((Arrow.Hom.right (f ≫ g)).app j) ⋯),
      naturality := ⋯ }
    (CategoryStruct.comp (Y :=
      { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
        map := fun {X Y_1 : J} (φ : X ⟶ Y_1) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Y.left.map φ) (Y.right.map φ) ⋯),
        map_id := ⋯, map_comp := ⋯ })
      {
        app := fun (j : J) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯),
        naturality := ⋯ }
      {
        app := fun (j : J) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯),
        naturality := ⋯ })
have w : ∀ (j : J),
  Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X_1 Y : J} (φ : X_1 ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (X.left.map φ) (X.right.map φ) sorry),
          map_id := sorry, map_comp := sorry }
        j)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y : J} (φ : X ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Z_1.left.map φ) (Z_1.right.map φ) sorry),
          map_id := sorry, map_comp := sorry }
        j))
    (NatTrans.app
      {
        app := fun (j : J) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂)
            (Arrow.homMk ((Arrow.Hom.left (f ≫ g)).app j) ((Arrow.Hom.right (f ≫ g)).app j) sorry),
        naturality := sorry }
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y_1 : J} (φ : X ⟶ Y_1) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Y.left.map φ) (Y.right.map φ) sorry),
          map_id := sorry, map_comp := sorry })
        {
          app := fun (j : J) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) sorry),
          naturality := sorry }
        {
          app := fun (j : J) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) sorry),
          naturality := sorry })
      j)
Tactic: ext j