-- 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)
dsimp :
  Eq (α :=
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).left ⟶ ((iteration I κ).obj (Arrow.mk f)).right)
    (CommaMorphism.left (CommaMorphism.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j))) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        CommaMorphism.right
            (NatTrans.app
              (NatTrans.app
                (TransfiniteCompositionOfShape.incl
                  (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
                    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
                j)
              (Arrow.mk f)) ≫
          𝟙 ((iteration I κ).obj (Arrow.mk f)).right)
    ((CommaMorphism.left
          (NatTrans.app
            (NatTrans.app
              (TransfiniteCompositionOfShape.incl
                (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
                  (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
              (Order.succ j))
            (Arrow.mk f)) ≫
        𝟙 ((iteration I κ).obj (Arrow.mk f)).left) ≫
      ((iteration I κ).obj (Arrow.mk f)).hom)
⊢ 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

Tactic:
dsimp [relativeCellComplexιObjFObjSuccIso,
    relativeCellComplexιObj, transfiniteCompositionOfShapeιIterationAppRight]

Premises used: CategoryTheory.SmallObject.relativeCellComplexιObj, CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRight, CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso