-- 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
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
rw :
  Eq (α :=
    extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
      F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (CategoryStruct.comp (Y := extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
      (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
        F.map (homOfLE ⋯) ≫ Iso.inv (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂)))
      (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫ F.map (homOfLE hi))
rw₁ :
  Eq (α :=
    extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
      F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
      CategoryStruct.comp (Y := extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
        (F.map (homOfLE ⋯) ≫ Iso.inv (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂)))
        (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫ F.map (homOfLE hi))
rw₂ :
  Eq (α :=
    extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
      F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
      F.map (homOfLE ⋯) ≫
        CategoryStruct.comp (Y :=
          extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
          (Iso.inv (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂)))
          (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫ F.map (homOfLE hi))
⊢ Eq (α :=
    extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
      F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (CategoryStruct.comp (Y := extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
        (extendToSucc.map hj F τ i₁ i₂ ⋯ ⋯)
        (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))) :
      extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
        F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫ F.map (homOfLE hi) :
      extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
        F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
have rw₃ : Eq (α :=
  extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ sorry) ⟶
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
  (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
    F.map (homOfLE sorry) ≫ 𝟙 (F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂)))
  (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫ F.map (homOfLE hi))
Tactic: rw [extendToSucc.map_eq _ _ _ _ _ _ hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]