awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f : X ⟶ Y
this₁ :
  ∀ (F : Arrow.{v, u} C ⥤ Arrow.{v, u} C), (propArrow I).functorCategory (Arrow.{v, u} C) ((succStruct I κ).toSucc F)
⊢ (succStruct I κ).prop f → (propArrow I).functorCategory (Arrow.{v, u} C) f

Tactic:
⟨F⟩
-- 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 κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f_1 : X ⟶ Y
F : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f : Arrow.{v, u} C
left : (coproducts.{w, v, u} I).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))
right : isomorphisms C (Arrow.Hom.right (((succStruct I κ).toSucc F).app f))
⊢ propArrow I (((succStruct I κ).toSucc F).app f)

Tactic:
constructor
-- 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 κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f_1 : X ⟶ Y
F : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f : Arrow.{v, u} C
left : (coproducts.{w, v, u} (ofHoms I.homFamily)).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))
⊢ (coproducts.{w, v, u} I).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))

Tactic:
nth_rw 1 [← I.ofHoms_homFamily]

Premises used: CategoryTheory.MorphismProperty.ofHoms_homFamily
-- 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 κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f_1 : X ⟶ Y
F : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f : Arrow.{v, u} C
left :
  coproducts.{w, v, u} (ofHoms I.homFamily) (X := ∐ functorObjSrcFamily I.homFamily (F.obj f).hom) (Y :=
    ∐ functorObjTgtFamily I.homFamily (F.obj f).hom)
    (functorObjLeft I.homFamily (F.obj f).hom :
      ∐ functorObjSrcFamily I.homFamily (F.obj f).hom ⟶ ∐ functorObjTgtFamily I.homFamily (F.obj f).hom)
⊢ (coproducts.{w, v, u} (ofHoms I.homFamily)).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))

Tactic:
apply pushouts_mk _ (functorObj_isPushout I.homFamily (F.obj f).hom)

Premises used: CategoryTheory.MorphismProperty.pushouts_mk, CategoryTheory.MorphismProperty.homFamily, CategoryTheory.Arrow.hom, CategoryTheory.SmallObject.functorObj_isPushout, CategoryTheory.Functor.obj
-- 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 κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f_1 : X ⟶ Y
F : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f : Arrow.{v, u} C
j : FunctorObjIndex I.homFamily (F.obj f).hom
⊢ ofHoms I.homFamily (X :=
    Functor.obj (Discrete.functor (functorObjSrcFamily I.homFamily (F.obj f).hom))
      { as := j : Discrete (FunctorObjIndex I.homFamily (F.obj f).hom) })
    (Y :=
    Functor.obj (Discrete.functor (functorObjTgtFamily I.homFamily (F.obj f).hom))
      { as := j : Discrete (FunctorObjIndex I.homFamily (F.obj f).hom) })
    (NatTrans.app
      (Discrete.natTrans fun (X : Discrete (FunctorObjIndex I.homFamily (F.obj f).hom)) ↦
        functorObjLeftFamily I.homFamily (F.obj f).hom X.as)
      { as := j })

Tactic:
constructor
-- 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 κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f_1 : X ⟶ Y
F : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f : Arrow.{v, u} C
⊢ coproducts.{w, v, u} (ofHoms I.homFamily) (X := ∐ functorObjSrcFamily I.homFamily (F.obj f).hom) (Y :=
    ∐ functorObjTgtFamily I.homFamily (F.obj f).hom)
    (functorObjLeft I.homFamily (F.obj f).hom :
      ∐ functorObjSrcFamily I.homFamily (F.obj f).hom ⟶ ∐ functorObjTgtFamily I.homFamily (F.obj f).hom)

Tactic:
exact coproducts_of_small _ _ (colimitsOfShape_colimMap _ (by rintro ⟨j⟩; constructor))

Premises used: CategoryTheory.MorphismProperty.coproducts_of_small, CategoryTheory.MorphismProperty.colimitsOfShape_colimMap
-- 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 κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f_1 : X ⟶ Y
F : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f : Arrow.{v, u} C
right : IsIso.{v, u} (𝟙 (F.obj f).right)
⊢ IsIso (Arrow.Hom.right (((succStruct I κ).toSucc F).app f))

Tactic:
dsimp [succStruct]

Premises used: CategoryTheory.SmallObject.succStruct
-- 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 κ
this_1 : LocallySmall.{w, v, u} C
this_2 : IsSmall.{w, v, u} I
this_3 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts.{v, u} C
X Y : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f_1 : X ⟶ Y
F : Arrow.{v, u} C ⥤ Arrow.{v, u} C
f : Arrow.{v, u} C
⊢ IsIso.{v, u} (𝟙 (F.obj f).right)

Tactic:
infer_instance
-- 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 κ
⊢ TransfiniteCompositionOfShape.F (Y := iteration I κ)
      (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
        (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)) =
    iterationFunctor I κ

Tactic:
rfl

Premises used: CategoryTheory.SmallObject.iterationFunctor, CategoryTheory.SmallObject.SuccStruct.iterationFunctor, rfl
-- 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 κ
f : Arrow.{v, u} C
⊢ IsIso (Y := ((iteration I κ).obj f).right) (Arrow.Hom.right (NatTrans.app (ιIteration I κ) f))

Tactic:
(transfiniteCompositionOfShapeιIterationAppRight I κ f).isIso

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.isIso, CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRight
-- 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 κ
j₁ j₂ : κ.ord.ToType
φ : j₁ ⟶ j₂
f : Arrow.{v, u} C
⊢ IsIso (Arrow.Hom.right (((iterationFunctor I κ).map φ).app f))

Tactic:
inferInstanceAs (IsIso ((transfiniteCompositionOfShapeιIterationAppRight I κ f).F.map φ))

Premises used: _private.0.CategoryTheory.SmallObject.instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor._proof_1
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
⊢ Eq (α := (((iterationFunctor I κ).obj j).obj f).right ⟶ ((iteration I κ).obj f).right)
    (Iso.hom (iterationFunctorObjObjRightIso I κ f j) ≫ Arrow.Hom.right (NatTrans.app (ιIteration I κ) f))
    (NatTrans.app
      (TransfiniteCompositionOfShape.incl
        (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := isomorphisms C)
          (transfiniteCompositionOfShapeιIterationAppRight I κ f)))
      j)

Tactic:
simp [iterationFunctorObjObjRightIso, iterationObjRightIso]

Premises used: CategoryTheory.SmallObject.iterationObjRightIso, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso
-- 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 κ
j : κ.ord.ToType
⊢ HasIterationOfShape.{w, v, u} κ.ord.ToType C

Tactic:
have := hasIterationOfShape I κ
-- 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 κ
j : κ.ord.ToType
this : HasIterationOfShape.{w, v, u} κ.ord.ToType C
⊢ NoMaxOrder.{w} κ.ord.ToType

Tactic:
have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
-- 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 κ
j : κ.ord.ToType
this_1 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
this : NoMaxOrder.{w} κ.ord.ToType
⊢ (succStruct I κ).prop (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE ⋯))

Tactic:
(succStruct I κ).prop_iterationFunctor_map_succ j (not_isMax j)

Premises used: not_isMax, CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ, CategoryTheory.SmallObject.succStruct
-- 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 κ
j : κ.ord.ToType
this_1 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
this : NoMaxOrder.{w} κ.ord.ToType
⊢ (succStruct I κ).prop (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE ⋯))

Tactic:
exact (succStruct I κ).prop_iterationFunctor_map_succ j (not_isMax j)

Premises used: not_isMax, CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ, CategoryTheory.SmallObject.succStruct
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
this_1 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
this : NoMaxOrder.{w} κ.ord.ToType
⊢ Eq (α :=
    (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f ⟶
      (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) (Order.succ j)).obj f)
    (NatTrans.app (Functor.map ((succStruct I κ).iterationFunctor κ.ord.ToType) (homOfLE ⋯)) f)
    (NatTrans.app
      ((succStruct I κ).toSucc (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j) ≫
        Iso.inv ((succStruct I κ).iterationFunctorObjSuccIso j ⋯))
      f)

Tactic:
have this := NatTrans.congr_app ((succStruct I κ).iterationFunctor_map_succ j (not_isMax j)) f
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
this_1 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
this_2 : NoMaxOrder.{w} κ.ord.ToType
this :
  Eq (α :=
    (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f ⟶
      (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) (Order.succ j)).obj f)
    (NatTrans.app (Functor.map ((succStruct I κ).iterationFunctor κ.ord.ToType) (homOfLE ⋯)) f)
    (NatTrans.app ((succStruct I κ).toSucc (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j)) f ≫
      NatTrans.app (Iso.inv ((succStruct I κ).iterationFunctorObjSuccIso j ⋯)) f)
dsimp :
  𝟙 ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f) ≫
      Arrow.homMk (ιFunctorObj I.homFamily ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f).hom)
        (𝟙 ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f).right) ⋯ =
    NatTrans.app (Functor.map ((succStruct I κ).iterationFunctor κ.ord.ToType) (homOfLE ⋯)) f ≫
      NatTrans.app (Iso.hom ((succStruct I κ).iterationFunctorObjSuccIso j ⋯)) f
⊢ Iso.hom
        (Iso.refl
          (Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
              (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f)).left) ≫
      (Arrow.mk (X := Functor.obj (𝟭 (Arrow.{v, u} C)) (((iterationFunctor I κ).obj j).obj f)) (Y :=
          (functor I.homFamily).obj (((iterationFunctor I κ).obj j).obj f))
          (NatTrans.app (ε I.homFamily) (((iterationFunctor I κ).obj j).obj f))).hom =
    (Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
          (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f)).hom ≫
      Iso.hom
        (Functor.mapIso (Functor.obj (evaluation (Arrow.{v, u} C) (Arrow.{v, u} C)) f)
          ((succStruct I κ).iterationFunctorObjSuccIso j ⋯))

Tactic:
dsimp [iterationFunctor]

Premises used: CategoryTheory.SmallObject.iterationFunctor
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
this_1 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
this_2 : NoMaxOrder.{w} κ.ord.ToType
this :
  Eq (α :=
    (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f ⟶
      (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) (Order.succ j)).obj f)
    (NatTrans.app (Functor.map ((succStruct I κ).iterationFunctor κ.ord.ToType) (homOfLE ⋯)) f)
    (NatTrans.app ((succStruct I κ).toSucc (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j)) f ≫
      NatTrans.app (Iso.inv ((succStruct I κ).iterationFunctorObjSuccIso j ⋯)) f)
rw :
  Arrow.homMk (ιFunctorObj I.homFamily ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f).hom)
      (𝟙 ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f).right) ⋯ =
    NatTrans.app ((succStruct I κ).toSucc (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j)) f
⊢ 𝟙 ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f) ≫
      Arrow.homMk (ιFunctorObj I.homFamily ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f).hom)
        (𝟙 ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f).right) ⋯ =
    NatTrans.app (Functor.map ((succStruct I κ).iterationFunctor κ.ord.ToType) (homOfLE ⋯)) f ≫
      NatTrans.app (Iso.hom ((succStruct I κ).iterationFunctorObjSuccIso j ⋯)) f

Tactic:
rw [id_comp, this, assoc, Iso.inv_hom_id_app, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
this_1 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
this_2 : NoMaxOrder.{w} κ.ord.ToType
this :
  Eq (α :=
    (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f ⟶
      (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) (Order.succ j)).obj f)
    (NatTrans.app (Functor.map ((succStruct I κ).iterationFunctor κ.ord.ToType) (homOfLE ⋯)) f)
    (NatTrans.app ((succStruct I κ).toSucc (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j)) f ≫
      NatTrans.app (Iso.inv ((succStruct I κ).iterationFunctorObjSuccIso j ⋯)) f)
⊢ Arrow.homMk (ιFunctorObj I.homFamily ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f).hom)
      (𝟙 ((Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j).obj f).right) ⋯ =
    NatTrans.app ((succStruct I κ).toSucc (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j)) f

Tactic:
dsimp [succStruct]

Premises used: CategoryTheory.SmallObject.succStruct
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
⊢ Arrow.Hom.left (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j)) =
    𝟙
      (Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
          (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f)).left

Tactic:
rfl

Premises used: Order.succ, rfl
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
⊢ Eq (α :=
    Functor.obj Arrow.rightFunc
        (Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
            (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f)).left ⟶
      Functor.obj Arrow.rightFunc
        (Arrow.mk (X := Functor.obj (𝟭 (Arrow.{v, u} C)) (((iterationFunctor I κ).obj j).obj f)) (Y :=
            (functor I.homFamily).obj (((iterationFunctor I κ).obj j).obj f))
            (NatTrans.app (ε I.homFamily) (((iterationFunctor I κ).obj j).obj f))).right)
    (Functor.map Arrow.rightFunc
      (Arrow.Hom.left (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j)) ≫
        (Arrow.mk (X := Functor.obj (𝟭 (Arrow.{v, u} C)) (((iterationFunctor I κ).obj j).obj f)) (Y :=
            (functor I.homFamily).obj (((iterationFunctor I κ).obj j).obj f))
            (NatTrans.app (ε I.homFamily) (((iterationFunctor I κ).obj j).obj f))).hom))
    (Functor.map Arrow.rightFunc
      ((Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
            (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f)).hom ≫
        Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j))))

Tactic:
have := Arrow.rightFunc.congr_map ((iterationFunctorMapSuccAppArrowIso I κ f j).hom.w)
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
this :
  Eq (α :=
    Functor.obj Arrow.rightFunc
        (Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
            (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f)).left ⟶
      Functor.obj Arrow.rightFunc
        (Arrow.mk (X := Functor.obj (𝟭 (Arrow.{v, u} C)) (((iterationFunctor I κ).obj j).obj f)) (Y :=
            (functor I.homFamily).obj (((iterationFunctor I κ).obj j).obj f))
            (NatTrans.app (ε I.homFamily) (((iterationFunctor I κ).obj j).obj f))).right)
    (Functor.map Arrow.rightFunc
      (Arrow.Hom.left (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j)) ≫
        (Arrow.mk (X := Functor.obj (𝟭 (Arrow.{v, u} C)) (((iterationFunctor I κ).obj j).obj f)) (Y :=
            (functor I.homFamily).obj (((iterationFunctor I κ).obj j).obj f))
            (NatTrans.app (ε I.homFamily) (((iterationFunctor I κ).obj j).obj f))).hom))
    (Functor.map Arrow.rightFunc
      ((Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
            (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f)).hom ≫
        Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j))))
dsimp :
  Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j))) ≫
      Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f) =
    𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right
⊢ Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j))) ≫
      Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f) =
    𝟙
      (Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
            (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f)).right.right

Tactic:
dsimp at this ⊢