-- 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₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ Eq (α :=
    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)) (Order.succ j) h))
    (if h₁ : Order.succ j ≤ j then
      Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
        F.map (homOfLE ⋯) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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) ≫
                𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
      (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
        F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂)))
      (if h₁ : Order.succ j ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ ⋯)) ≫
          F.map (homOfLE h₂₃) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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) ≫
                  𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
        else eqToHom ⋯))
have neg : Eq (α :=
  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)) (Order.succ j) h))
  (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) ≫
            𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
  else eqToHom sorry)
  (CategoryStruct.comp (Y := obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ sorry))
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
      F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂)))
    (if h₁ : Order.succ j ≤ j then
      Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ sorry)) ≫
        F.map (homOfLE h₂₃) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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) ≫
                𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
      else eqToHom sorry))
Tactic: rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂, assoc, assoc,
        Iso.inv_hom_id_assoc, comp_id, ← Functor.map_comp_assoc, homOfLE_comp]