-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
lemma πFunctorObj_eq (j : κ.ord.toType) :
    letI := hasColimitsOfShape_discrete I κ
    letI := hasPushouts I κ
    πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
      (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
      πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.toType
h₁ :
  (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.right
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        (((transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j).app (Arrow.mk f)).right ≫
          𝟙 ((iteration I κ).obj (Arrow.mk f)).right =
    ((((transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j)).app (Arrow.mk f)).left ≫
        𝟙 ((iteration I κ).obj (Arrow.mk f)).left) ≫
      ((iteration I κ).obj (Arrow.mk f)).hom

Tactic:
simp only [reassoc_of% h₁, comp_id, comp_id, Arrow.w_mk_right, ← h₂,
  NatTrans.comp_app, Arrow.comp_right,
  iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.toType
h₁ :
  (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.right
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        (transfiniteCompositionOfShapeιIterationAppRight I κ (Arrow.mk f)).incl.app j =
    (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ ((iteration I κ).obj (Arrow.mk f)).hom

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

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.toType
h₁ :
  (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.right
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        (((transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j).app (Arrow.mk f)).right ≫
          𝟙 ((iteration I κ).obj (Arrow.mk f)).right =
    ((((transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j)).app (Arrow.mk f)).left ≫
        𝟙 ((iteration I κ).obj (Arrow.mk f)).left) ≫
      ((iteration I κ).obj (Arrow.mk f)).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.toType
h₁ :
  (𝟭 C).map (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj (Arrow.mk f)))).right.hom =
    (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app (Arrow.mk f))).right.hom ≫
      (𝟭 C).map (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.right
h₂ :
  (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).F.map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j ≫
      ((Functor.const κ.ord.toType).obj (iteration I κ)).map (homOfLE ⋯)
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Tactic:
dsimp at h₁ h₂

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.toType
h₁ :
  (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.right
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j ≫ 𝟙 (iteration I κ)
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv