-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j))) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j)))
h₂ :
  Eq (α := (iterationFunctor I κ).obj j ⟶ iteration I κ)
    (CategoryStruct.comp (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE ⋯))
      (NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
            (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
        (Order.succ j)))
    (NatTrans.app
      (TransfiniteCompositionOfShape.incl
        (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
          (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
      j)
rw :
  Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        NatTrans.app
          (TransfiniteCompositionOfShape.incl
            (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := isomorphisms C)
              (transfiniteCompositionOfShapeιIterationAppRight I κ (Arrow.mk f))))
          j =
    NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f)))
        (Order.succ j) ≫
      ((iteration I κ).obj (Arrow.mk f)).hom
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    Iso.inv (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      NatTrans.app
          (TransfiniteCompositionOfShape.incl
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f)))
          (Order.succ j) ≫
        πObj I κ f ≫ Iso.inv (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j)

Tactic:
rw [← cancel_mono (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom,
    ← cancel_mono ((ιIteration I κ).app f).right, assoc, assoc, assoc, assoc, assoc,
    Iso.inv_hom_id_assoc, πObj_ιIteration_app_right,
    iterationFunctorObjObjRightIso_ιIteration_app_right,
    ← cancel_epi (relativeCellComplexιObjFObjSuccIso I κ f j).hom, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SmallObject.πObj_ιIteration_app_right, CategoryTheory.SmallObject.ιIteration, CategoryTheory.Arrow.Hom.right, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso, CategoryTheory.Arrow.mk, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app