-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
inl :
  ∀ (hi₃' : i₃ < j),
    Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (CategoryStruct.comp (Y := obj c i₂)
        (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
        else
          if h₁ : i₁ < j then
            (objIso c i₁ h₁).hom ≫
              c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
          else eqToHom ⋯)
        (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
        else
          if h₁ : i₂ < j then
            (objIso c i₂ h₁).hom ≫
              c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
          else eqToHom ⋯))
⊢ Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))
have inl₁ : ∀ {F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₃) : Type u) C} (c : Cocone F) (hi₃ : i₃ ≤ i₃),
  Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (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 sorry
      else eqToHom sorry)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < i₃ then Iso.hom (objIso c i₁ sorry) ≫ 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 sorry
        else eqToHom sorry)
      (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₂ sorry) ≫ 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 sorry
        else eqToHom sorry))
Tactic: obtain hi₃' | rfl := hi₃.lt_or_eq
Cleared hypotheses: j, F, c, hi₃