-- 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
obtain :
  ∀
    (l :
      (↑(Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ I.toSet) (Arrow.mk i) hi) : Arrow C).right ⟶
        (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))
    (hl₁ :
      I.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ I.toSet) (Arrow.mk i) hi) ≫ l =
        t ≫
          (TransfiniteCompositionOfShape.F (Y := obj I κ f)
                (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
                  (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).map
            (homOfLE ⋯))
    (hl₂ :
      l ≫
          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 =
        b),
    sq.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := ιFunctorObj_extension' I.homFamily
    ((relativeCellComplexιObj I κ f).incl.app j ≫ πObj I κ f)
    ((relativeCellComplexιObj I κ f).F.map (homOfLE (Order.le_succ j)))
    ((relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f) (by simp) (Iso.refl _)
    (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).symm
    (relativeCellComplexιObjFObjSuccIso I κ f j)
    (by dsimp; rw [ιFunctorObj_eq, id_comp])
    (by dsimp; rw [πFunctorObj_eq, assoc, Iso.hom_inv_id_assoc])
    (i := ⟨i, hi⟩) t b (by rw [reassoc_of% ht, sq.w]; dsimp)

Premises used: CategoryTheory.SmallObject.relativeCellComplexιObj, Order.succ, CategoryTheory.MorphismProperty.homFamily, CategoryTheory.Iso.refl, CategoryTheory.TransfiniteCompositionOfShape.incl, CategoryTheory.TransfiniteCompositionOfShape.F, CategoryTheory.SmallObject.πObj, CategoryTheory.Functor.map, CategoryTheory.SmallObject.ιFunctorObj_extension', CategoryTheory.homOfLE, CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso, Order.le_succ, CategoryTheory.Arrow.mk, HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape, CategoryTheory.NatTrans.app