-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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
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 φ) ⋯),
            map_id := ⋯, map_comp := ⋯ }
          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 φ) ⋯),
            map_id := ⋯, map_comp := ⋯ }
          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) ⋯),
          naturality := ⋯ }
        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 φ) ⋯),
            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 := ⋯ })
        j)
⊢ 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 := ⋯ })

Tactic:
ext j