∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ : f.obj' 0 _proof_353✝ ⟶ g.obj' 0 _proof_353✝) (app₁ : f.obj' 1 _proof_354✝ ⟶ g.obj' 1 _proof_354✝)
  (app₂ : f.obj' 2 _proof_355✝ ⟶ g.obj' 2 _proof_355✝) (app₃ : f.obj' 3 _proof_356✝ ⟶ g.obj' 3 _proof_356✝)
  (app₄ : f.obj' 4 _proof_357✝ ⟶ g.obj' 4 _proof_357✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_354✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_354✝))
      _auto_397✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝ _proof_355✝))
      _auto_399✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝ _proof_356✝))
      _auto_401✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_357✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝ _proof_357✝))
      _auto_403✝),
  (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app
      ⟨4, CategoryTheory.ComposableArrows.homMk₄._proof_5⟩ =
    app₄