-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (goal)
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)
⊢ 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
have 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)
Tactic: dsimp [relativeCellComplexιObjFObjSuccIso,
    relativeCellComplexιObj, transfiniteCompositionOfShapeιIterationAppRight]