-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
@[reassoc (attr := simp)]
lemma iterationFunctorMapSuccAppArrowIso_hom_right_right_comp
    (f : Arrow C) (j : κ.ord.toType) :
    (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right ≫
      (((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f).right = 𝟙 _

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 κ
f : Arrow C
j : κ.ord.toType
this :
  Arrow.rightFunc.map
      ((𝟭 (Arrow C)).map (iterationFunctorMapSuccAppArrowIso I κ f j).hom.left ≫
        (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj f))).hom) =
    Arrow.rightFunc.map
      ((Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).hom ≫
        (𝟭 (Arrow C)).map (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right)
⊢ (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right ≫
      (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right =
    𝟙 (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).right.right

Tactic:
dsimp at this ⊢

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.toType
this :
  𝟙 (((iterationFunctor I κ).obj j).obj f).right ≫ 𝟙 (((iterationFunctor I κ).obj j).obj f).right =
    (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right ≫
      (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right
⊢ (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right ≫
      (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right =
    𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right

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 κ
f : Arrow C
j : κ.ord.toType
this :
  𝟙 (((iterationFunctor I κ).obj j).obj f).right ≫ 𝟙 (((iterationFunctor I κ).obj j).obj f).right =
    (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right ≫
      (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right
⊢ (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right ≫
      (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right =
    𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right

Tactic:
rw [← cancel_epi (((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f).right,
  ← reassoc_of% this, comp_id]

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 κ
f : Arrow C
j : κ.ord.toType
⊢ (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right ≫
      (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right =
    𝟙 (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).right.right

Tactic:
have := Arrow.rightFunc.congr_map ((iterationFunctorMapSuccAppArrowIso I κ f j).hom.w)

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.toType
this :
  Arrow.rightFunc.map
      ((𝟭 (Arrow C)).map (iterationFunctorMapSuccAppArrowIso I κ f j).hom.left ≫
        (Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj f))).hom) =
    Arrow.rightFunc.map
      ((Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).hom ≫
        (𝟭 (Arrow C)).map (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right)
⊢ (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right ≫
      (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right =
    𝟙 (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).right.right