-- 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 A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this_1 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this_2 : HasPushouts.{v, u} C
this :
  PreservesColimit
    (TransfiniteCompositionOfShape.F (Y := obj I κ f)
      (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦ (↑I.toSet : Type (max u v)))
        (relativeCellComplexιObj I κ f)))
    (Functor.obj coyoneda (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t :
  A ⟶
    (TransfiniteCompositionOfShape.F (Y := obj I κ f)
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).obj
      j
ht :
  t ≫
      NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f)))
        j =
    g
rw :
  Eq (α :=
    (TransfiniteCompositionOfShape.F (Y := obj I κ f)
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).obj
        (Order.succ j) ⟶
      (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).right)
    ((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))
    (Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      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))
rw₁ :
  Eq (α :=
    (TransfiniteCompositionOfShape.F (Y := obj I κ f)
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).obj
        (Order.succ j) ⟶
      (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).right)
    (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))
    (Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      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))
rw₂ rw₃ :
  Eq (α :=
    (TransfiniteCompositionOfShape.F (Y := obj I κ f)
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).obj
        (Order.succ j) ⟶
      (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).right)
    (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))
    (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))
⊢ (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) =
    Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom

Tactic:
rw [πFunctorObj_eq, assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SmallObject.πFunctorObj_eq, CategoryTheory.Iso.hom_inv_id_assoc