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 κ
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
rw₁ :
  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
rw₂ rw₃ :
  Eq (α := (((iterationFunctor I κ).obj j).obj f).right ⟶ (((iterationFunctor I κ).obj (Order.succ j)).obj f).right)
    (Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) f))
    (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) =
    𝟙 (((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]

Premises used: CategoryTheory.Arrow.Hom.right, CategoryTheory.SmallObject.iterationFunctor, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.homOfLE, Order.le_succ, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app
-- 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 : C
f : X ⟶ Y
⊢ πObj I κ f ≫ Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk f)) = ((iteration I κ).obj (Arrow.mk f)).hom

Tactic:
simp [πObj]

Premises used: CategoryTheory.SmallObject.π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 κ
X Y : C
f : X ⟶ Y
⊢ CategoryStruct.comp (Y := obj I κ f) (ιObj I κ f) (πObj I κ f) = f

Tactic:
simp [ιObj, πObj]

Premises used: CategoryTheory.SmallObject.ιObj, CategoryTheory.SmallObject.π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 κ
X Y : C
f : X ⟶ Y
⊢ 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 κ
X Y : C
f : X ⟶ Y
this : HasIterationOfShape.{w, v, u} κ.ord.ToType C
h : (succStruct I κ).prop.TransfiniteCompositionOfShape κ.ord.ToType (Y := iteration I κ) (ιIteration I κ) :=
  transfiniteCompositionOfShapeSuccStructPropιIteration I κ
⊢ RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦ (↑I.toSet : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑I.toSet : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑I.toSet : Type (max u v))) ↦ (↑i : Arrow C).right) fun (x : κ.ord.ToType) ↦
    I.homFamily (Y := obj I κ f) (ιObj I κ f)

Tactic:
exact
  { toTransfiniteCompositionOfShape :=
      h.toTransfiniteCompositionOfShape.map ((evaluation _ _).obj f ⋙ Arrow.leftFunc)
    attachCells j hj :=
      attachCellsOfSuccStructProp I κ (h.map_mem j hj) 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 κ
X Y : C
f : X ⟶ Y
⊢ (coproducts.{w, v, u} (ofHoms I.homFamily)).pushouts ≤ (coproducts.{w, v, u} I).pushouts

Tactic:
simp
-- 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 : C
f : X ⟶ Y
a :
  transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType (Y := obj I κ f) (ιObj I κ f)
⊢ I.rlp.llp (Y := obj I κ f) (ιObj I κ f)

Tactic:
apply I.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp κ.ord.ToType

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, Cardinal.ord, Ordinal.ToType
-- 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 : C
f : X ⟶ Y
⊢ transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType (Y := obj I κ f) (ιObj I κ f)

Tactic:
apply transfiniteCompositionsOfShape_ιObj

Premises used: CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ι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 κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
⊢ ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (TransfiniteCompositionOfShape.F (Y := obj I κ f)
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).map
        (homOfLE ⋯) ≫
      Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j)

Tactic:
simpa using Arrow.leftFunc.congr_map (iterationFunctorMapSuccAppArrowIso I κ f j).hom.w

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

Tactic:
have h₁ := (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.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 κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j))) ≫
      (Arrow.mk (X := Functor.obj (𝟭 (Arrow.{v, u} C)) (((iterationFunctor I κ).obj j).obj (Arrow.mk f))) (Y :=
            (functor I.homFamily).obj (((iterationFunctor I κ).obj j).obj (Arrow.mk f)))
            (NatTrans.app (ε I.homFamily) (((iterationFunctor I κ).obj j).obj (Arrow.mk f)))).right.hom =
    (Arrow.mk (X := ((iterationFunctor I κ).obj j).obj (Arrow.mk f)) (Y :=
            ((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f))
            (NatTrans.app ((iterationFunctor I κ).map (homOfLE ⋯)) (Arrow.mk f))).right.hom ≫
      Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j)))
⊢ Eq (α :=
    (TransfiniteCompositionOfShape.F (Y := iteration I κ)
            (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
              (transfiniteCompositionOfShapeSuccStructPropιIteration I κ))).obj
        j ⟶
      Functor.obj (Functor.obj (Functor.const κ.ord.ToType) (iteration I κ)) (Order.succ j))
    ((TransfiniteCompositionOfShape.F (Y := iteration I κ)
            (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
              (transfiniteCompositionOfShapeSuccStructPropιIteration I κ))).map
        (homOfLE ⋯) ≫
      NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
            (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
        (Order.succ j))
    (NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
            (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
        j ≫
      Functor.map (Functor.obj (Functor.const κ.ord.ToType) (iteration I κ)) (homOfLE ⋯))

Tactic:
have h₂ := (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.naturality
    (homOfLE (Order.le_succ j))
-- 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 : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j))) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j)))
h₂ :
  Eq (α := (iterationFunctor I κ).obj j ⟶ iteration I κ)
    (CategoryStruct.comp (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE ⋯))
      (NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
            (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
        (Order.succ j)))
    (NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
            (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
        j ≫
      𝟙 (iteration I κ))
⊢ Eq (α := (iterationFunctor I κ).obj j ⟶ iteration I κ)
    (CategoryStruct.comp (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE ⋯))
      (NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
            (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
        (Order.succ j)))
    (NatTrans.app
      (TransfiniteCompositionOfShape.incl
        (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
          (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
      j)

Tactic:
rw [comp_id] at h₂

Premises used: CategoryTheory.Category.comp_id
-- 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 : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j))) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j)))
h₂ :
  Eq (α := (iterationFunctor I κ).obj j ⟶ iteration I κ)
    (CategoryStruct.comp (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE ⋯))
      (NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
            (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
        (Order.succ j)))
    (NatTrans.app
      (TransfiniteCompositionOfShape.incl
        (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
          (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
      j)
⊢ Eq (α :=
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).left ⟶ ((iteration I κ).obj (Arrow.mk f)).right)
    (CommaMorphism.left (CommaMorphism.right (Iso.hom (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j))) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        CommaMorphism.right
            (NatTrans.app
              (NatTrans.app
                (TransfiniteCompositionOfShape.incl
                  (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
                    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
                j)
              (Arrow.mk f)) ≫
          𝟙 ((iteration I κ).obj (Arrow.mk f)).right)
    ((CommaMorphism.left
          (NatTrans.app
            (NatTrans.app
              (TransfiniteCompositionOfShape.incl
                (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := (succStruct I κ).prop)
                  (transfiniteCompositionOfShapeSuccStructPropιIteration I κ)))
              (Order.succ j))
            (Arrow.mk f)) ≫
        𝟙 ((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]

Premises used: CategoryTheory.Arrow.w_mk_right, CategoryTheory.Category.comp_id, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, CategoryTheory.NatTrans.comp_app, CategoryTheory.Arrow.comp_right
-- 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
⊢ ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
haveI := hasColimitsOfShape_discrete 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 κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
⊢ HasPushouts.{v, u} C

Tactic:
haveI := hasPushouts 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 κ
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 : HasPushouts.{v, u} C
⊢ 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))

Tactic:
haveI := preservesColimit I κ i hi _ (relativeCellComplexιObj I κ 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 κ
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
obtain :
  ∀ (j : κ.ord.ToType)
    (t :
      (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)).obj
        j)
    (ht :
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone (Functor.obj coyoneda (Opposite.op A))
                    { pt := obj I κ f,
                      ι :=
                        TransfiniteCompositionOfShape.incl
                          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
                            (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f)) :
                      Cocone
                        (TransfiniteCompositionOfShape.F (Y := obj I κ f)
                          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
                            (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))) }))
                j) :
            (a : (fun (X : Type v) ↦ X) (((relativeCellComplexιObj I κ f).F ⋙ coyoneda.obj (Opposite.op A)).obj j)) →
              (fun (X : Type v) ↦ X)
                (((Functor.const κ.ord.ToType).obj
                      ((coyoneda.obj (Opposite.op A)).mapCocone
                          { pt := obj I κ f, ι := (relativeCellComplexιObj I κ f).incl }).pt).obj
                  j))
          t =
        g),
    sq.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨j, t, ht⟩ := Types.jointly_surjective _
    (isColimitOfPreserves (coyoneda.obj (Opposite.op A))
      (relativeCellComplexιObj I κ f).isColimit) g

Premises used: CategoryTheory.SmallObject.relativeCellComplexιObj, CategoryTheory.coyoneda, Opposite.op, CategoryTheory.Limits.Types.jointly_surjective, CategoryTheory.TransfiniteCompositionOfShape.isColimit, HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- 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
⊢ CategoryStruct.comp (Y :=
      (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))
      ((TransfiniteCompositionOfShape.F (Y := obj I κ f)
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).map
        (homOfLE ⋯))
      (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) =
    NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f)))
        j ≫
      πObj I κ f

Tactic:
simp