-- 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 : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
τ : X ⟶ Y
x x_1 : J
x_2 : x ⟶ x_1
⊢ 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 := ⋯ }
        x)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { 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 := ⋯ }
        x_1))
    (Functor.map
        { 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 := ⋯ : Functor.{v_3, v_1, u_3, u_1} J C }
        x_2 ≫
      data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) ⋯))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_3, v_1, u_3, u_1}
        { 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 := ⋯ }
        x)
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) ⋯))
      (Functor.map
        { 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 := ⋯ }
        x_2))
have dsimp : Eq (α :=
  (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app x)).Z (W₁ := W₁) (W₂ := W₂) ⟶
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app x_1)).Z (W₁ := W₁) (W₂ := W₂))
  (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app x_1)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (X.left.map x_2) (X.right.map x_2) sorry))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) sorry)))
  (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app x)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) sorry))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Y.left.map x_2) (Y.right.map x_2) sorry)))
Tactic: dsimp