-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i : J
hi : i ≤ Order.succ j
pos :
  ∀ (h₁ : i ≤ j),
    Eq.{v_1 + 1} (α :=
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
        obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
      (if h₁ : i ≤ j then
        CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
          (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)))
          (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) ≫
            Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)))
      else
        if h₂ : i ≤ j then
          Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₂)) ≫
            F.map (homOfLE h₂) ≫ τ ≫ Iso.inv (objSuccIso hj F X) ≫ eqToHom ⋯
        else 𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
      (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
⊢ Eq.{v_1 + 1} (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (if h₁ : i ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)))
    else
      if h₂ : i ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₂)) ≫
          F.map (homOfLE h₂) ≫ τ ≫ Iso.inv (objSuccIso hj F X) ≫ eqToHom ⋯
      else 𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
have neg : ∀ (h₁ : ¬i ≤ j),
  Eq.{v_1 + 1} (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (if h₁ : i ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)))
    else
      if h₂ : i ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₂)) ≫
          F.map (homOfLE h₂) ≫ τ ≫ Iso.inv (objSuccIso hj F X) ≫ eqToHom sorry
      else 𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry)))
Tactic: by_cases h₁ : i ≤ j