-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₃) : Type u) C
c : Cocone F
hi₃ : i₃ ≤ i₃
inl :
  Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₁ : i₁ < i₃ then
      (objIso c i₁ h₁).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
    else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < i₃ then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < i₃ then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < i₃ then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))
inl₁ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv ≫ eqToHom ⋯) =
    CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < i₃ then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < i₃ then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < i₃ then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
inl₂ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv ≫ eqToHom ⋯) =
    (Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫
      if h₂ : i₃ < i₃ then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < i₃ then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯
inl₃ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv ≫ eqToHom ⋯) =
    (Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫
      if h₁ : i₂ < i₃ then
        (objIso c i₂ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯
inl₄ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv ≫ eqToHom ⋯) =
    (Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫
      (objIso c i₂ hi₂₃).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ hi₂₃) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
inl₅ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv ≫ 𝟙 (obj c i₃)) =
    (Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫
      (objIso c i₂ hi₂₃).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ hi₂₃) ≫ (objIsoPt c).inv ≫ 𝟙 (obj c i₃)
inl₆ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv) =
    (Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫
      (objIso c i₂ hi₂₃).hom ≫ c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ hi₂₃) ≫ (objIsoPt c).inv
inl₇ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv) =
    Iso.hom (objIso c i₁ ⋯) ≫
      (F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫
        (objIso c i₂ hi₂₃).hom ≫ c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ hi₂₃) ≫ (objIsoPt c).inv
inl₈ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv) =
    Iso.hom (objIso c i₁ ⋯) ≫
      F.map (homOfLE hi) ≫
        (objIso c i₂ hi₂₃).inv ≫
          (objIso c i₂ hi₂₃).hom ≫ c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ hi₂₃) ≫ (objIsoPt c).inv
inl₉ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv) =
    Iso.hom (objIso c i₁ ⋯) ≫
      F.map (homOfLE hi) ≫ c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ hi₂₃) ≫ (objIsoPt c).inv
inl₁₀ inl₁₁ :
  CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv) =
    CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯)) (Iso.hom (objIso c i₁ ⋯))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ ⋯) ≫ (objIsoPt c).inv)
⊢ Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < i₃ then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < i₃ then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < i₃ then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < i₃ then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))

Tactic:
rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp),
          dif_pos hi₂₃, eqToHom_refl, comp_id, assoc, assoc, Iso.inv_hom_id_assoc,
          Cocone.w_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.w_assoc, dif_pos, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, dif_neg, LT.lt.trans