awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow.{v, u} C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ Arrow.Hom.left (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯) =
    Arrow.Hom.left
      (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯)
have h₁ : Eq (α := functorObj f π₁.hom ⟶ functorObj f π₃.hom) (functorMap f (τ ≫ τ'))
  (CategoryStruct.comp (Y := functorObj f π₂.hom) (functorMap f τ) (functorMap f τ'))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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
p : X ⟶ Y
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
have this : LocallySmall.{w, v, u} C
Tactic: haveI := locallySmall I κ
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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
p : X ⟶ Y
this : LocallySmall.{w, v, u} C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
have this₁ : IsSmall.{w, v, u} I
Tactic: haveI := isSmall I κ
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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
p : X ⟶ Y
this_1 : LocallySmall.{w, v, u} C
this : IsSmall.{w, v, u} I
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
have this₁ : HasCoproducts.{w, v, u} C
Tactic: haveI := hasCoproducts I κ
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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 κ
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow.{v, u} C)
have this : LocallySmall.{w, v, u} C
Tactic: haveI := locallySmall I κ
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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 : LocallySmall.{w, v, u} C
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow.{v, u} C)
have this₁ : IsSmall.{w, v, u} I
Tactic: haveI := isSmall I κ
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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 : IsSmall.{w, v, u} I
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow.{v, u} C)
have this₁ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
Tactic: haveI := hasColimitsOfShape_discrete I κ
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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 : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow.{v, u} C)
have this₁ : HasPushouts.{v, u} C
Tactic: haveI := hasPushouts I κ
-- 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 κ
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
⊢ (succStruct I κ).prop f → (propArrow I).functorCategory (Arrow.{v, u} C) f
have this₁ : ∀ (F : Arrow.{v, u} C ⥤ Arrow.{v, u} C), (propArrow I).functorCategory (Arrow.{v, u} C) ((succStruct I κ).toSucc F)
Tactic: ⟨F⟩
-- 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 κ
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
⊢ propArrow I (((succStruct I κ).toSucc F).app f)
have left : (coproducts.{w, v, u} I).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))
Tactic: constructor
-- 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 κ
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))
⊢ propArrow I (((succStruct I κ).toSucc F).app f)
have right : isomorphisms C (Arrow.Hom.right (((succStruct I κ).toSucc F).app f))
Tactic: constructor
-- 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 κ
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} I).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))
have left : (coproducts.{w, v, u} (ofHoms I.homFamily)).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))
Tactic: nth_rw 1 [← I.ofHoms_homFamily]
-- 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 κ
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)).pushouts (Arrow.Hom.left (((succStruct I κ).toSucc F).app f))
have 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)
Tactic: apply pushouts_mk _ (functorObj_isPushout I.homFamily (F.obj f).hom)
-- 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 κ
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 (Arrow.Hom.right (((succStruct I κ).toSucc F).app f))
have right : IsIso.{v, u} (𝟙 (F.obj f).right)
Tactic: dsimp [succStruct]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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
⊢ (succStruct I κ).prop (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE ⋯))
have this : HasIterationOfShape.{w, v, u} κ.ord.ToType C
Tactic: have := hasIterationOfShape I κ
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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
⊢ (succStruct I κ).prop (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE ⋯))
have this₁ : NoMaxOrder.{w} κ.ord.ToType
Tactic: have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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
⊢ 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 ⋯))
have 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 sorry)) f)
  (NatTrans.app
    ((succStruct I κ).toSucc (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j) ≫
      Iso.inv ((succStruct I κ).iterationFunctorObjSuccIso j sorry))
    f)
Tactic: have this := NatTrans.congr_app ((succStruct I κ).iterationFunctor_map_succ j (not_isMax j)) f
-- 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 κ
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)
⊢ 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 ⋯))
have 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) sorry =
  NatTrans.app (Functor.map ((succStruct I κ).iterationFunctor κ.ord.ToType) (homOfLE sorry)) f ≫
    NatTrans.app (Iso.hom ((succStruct I κ).iterationFunctorObjSuccIso j sorry)) f
Tactic: dsimp [iterationFunctor]
-- 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 κ
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)
⊢ 𝟙 ((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
have 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) sorry =
  NatTrans.app ((succStruct I κ).toSucc (Functor.obj ((succStruct I κ).iterationFunctor κ.ord.ToType) j)) f
Tactic: rw [id_comp, this, assoc, Iso.inv_hom_id_app, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
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.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
have this : Eq (α :=
  Functor.obj Arrow.rightFunc
      (Arrow.mk (Y := ((iterationFunctor I κ).obj (Order.succ j)).obj f)
          (NatTrans.app ((iterationFunctor I κ).map (homOfLE sorry)) 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 sorry)) f)).hom ≫
      Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j))))
Tactic: have := Arrow.rightFunc.congr_map ((iterationFunctorMapSuccAppArrowIso I κ f j).hom.w)
-- 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 κ
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))))
⊢ 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
have dsimp : Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j))) ≫
    Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE sorry)) f) =
  𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right
Tactic: dsimp at this ⊢
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
this :
  𝟙 (((iterationFunctor I κ).obj j).obj f).right ≫ 𝟙 (((iterationFunctor I κ).obj j).obj f).right =
    Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f) ≫
      Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j)))
⊢ 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
have rw : Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE sorry)) f) ≫
    Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j))) ≫
      Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE sorry)) f) =
  Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE sorry)) f) ≫
    𝟙 (((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]
-- 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 κ
f : Arrow.{v, u} C
j : κ.ord.ToType
this :
  𝟙 (((iterationFunctor I κ).obj j).obj f).right ≫ 𝟙 (((iterationFunctor I κ).obj j).obj f).right =
    Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f) ≫
      Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j)))
rw :
  Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f) ≫
      Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ f j))) ≫
        Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f) =
    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) =
    𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right
have rw₁ : Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE sorry)) f) =
  Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE sorry)) f) ≫
    𝟙 (((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]