-- 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
h₁ : i ≤ j
pos :
  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)) i hi))
    (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₁))) :
      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))
    (𝟙 (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 ⋯) ⟶
        obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
pos₁ :
  Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) ≫
      𝟙 (F.obj (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₁)) =
    𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
pos₂ :
  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)) i hi))
    (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 ⋯)))
        (Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁))) :
      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))
    (𝟙 (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 ⋯) ⟶
        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 pos₃ : 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))
  (𝟙 (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: rw [dif_pos h₁, CategoryTheory.Functor.map_id, id_comp, Iso.hom_inv_id]