-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
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))
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 ⋯) ≫ 𝟙 (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))
rw₄ 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 ⋯))
    (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₂))

Tactic:
rw [extendToSucc.map_eq _ _ _ _ _ _ hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_eq, CategoryTheory.Category.comp_id