-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
rw :
  arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  Arrow.mk (X := (iter i ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)) (Y :=
      Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) (Order.succ i) ⋯))
      ((iter i ⋯).mapObj (iter (Order.succ i) ⋯) ⋯ ⋯ ⋯ ⋯) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₂ :
  arrowMap (F (iter (Order.succ i) ⋯)) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₃ :
  arrowSucc (j := Order.succ i) (F (iter (Order.succ i) ⋯)) i ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₄ :
  Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₅ :
  Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)) =
    Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
iter' : Φ.Iteration (Order.succ i)
hk : i ≤ Order.succ i
rw₆ : J
rw₇ :
  Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)) =
    Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
iter'₁ : Φ.Iteration (Order.succ i)
hk₁ : i ≤ Order.succ i
rw₈ : J
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))

Tactic:
rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ hi]

Premises used: Iff.mpr, Order.IsSuccLimit.succ_lt_iff, not_isMax_of_lt, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor_obj, Order.lt_succ_of_le_of_not_isMax, Order.le_succ, CategoryTheory.SmallObject.SuccStruct.arrowSucc_def, CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj