∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_441✝ ⟶ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ⟶ g.obj' 1 _proof_442✝¹)
  (app₂ : f.obj' 2 _proof_443✝ ⟶ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ⟶ g.obj' 3 _proof_444✝¹)
  (app₄ : f.obj' 4 _proof_445✝ ⟶ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ⟶ g.obj' 5 _proof_446✝¹)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_442✝²)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_442✝³))
      _auto_483✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_443✝³))
      _auto_485✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_444✝³))
      _auto_487✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝¹ _proof_445✝³))
      _auto_489✝)
  (w₄ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅ =
        CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_445✝⁵ _proof_446✝³))
      _auto_491✝),
  (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app
      ⟨3, CategoryTheory.ComposableArrows.homMk₅._proof_4⟩ =
    app₃