∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄),
  CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄ →
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).map' 2 3 _proof_291✝ _proof_292✝)
        f₄ =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj' 2 _proof_291✝¹))
        ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃₄).map' 2 3 _proof_291✝² _proof_292✝¹)