awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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₂ : 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 sorry)) f))
  (Arrow.Hom.right (NatTrans.app ((iterationFunctor I κ).map (homOfLE sorry)) f))
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 (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
f : X ⟶ Y
⊢ 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)
have this : HasIterationOfShape.{w, v, u} κ.ord.ToType C
Tactic: have := hasIterationOfShape 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 κ
X Y : C
f : X ⟶ Y
⊢ I.rlp.llp (Y := obj I κ f) (ιObj I κ f)
have a : transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType (Y := obj I κ f) (ιObj I κ f)
Tactic: apply I.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp κ.ord.ToType
-- 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
f : X ⟶ Y
j : κ.ord.ToType
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    Iso.inv (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      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 ≫ Iso.inv (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j)
have 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 sorry)) (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
-- 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
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)))
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    Iso.inv (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      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 ≫ Iso.inv (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j)
have h₂ : 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 sorry) ≫
    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 sorry))
Tactic: have h₂ := (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.naturality
    (homOfLE (Order.le_succ j))
-- 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
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 κ))
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    Iso.inv (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      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 ≫ Iso.inv (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j)
have h₃ : Eq (α := (iterationFunctor I κ).obj j ⟶ iteration I κ)
  (CategoryStruct.comp (Y := (iterationFunctor I κ).obj (Order.succ j)) ((iterationFunctor I κ).map (homOfLE sorry))
    (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₂
Cleared hypotheses: h₂
-- 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 κ
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)
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    Iso.inv (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      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 ≫ Iso.inv (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j)
have rw : Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
    πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
      NatTrans.app
        (TransfiniteCompositionOfShape.incl
          (TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape (W := isomorphisms C)
            (transfiniteCompositionOfShapeιIterationAppRight I κ (Arrow.mk f))))
        j =
  NatTrans.app
      (TransfiniteCompositionOfShape.incl
        (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦ (↑I.toSet : Type (max u v)))
          (relativeCellComplexιObj I κ f)))
      (Order.succ j) ≫
    ((iteration I κ).obj (Arrow.mk f)).hom
Tactic: rw [← cancel_mono (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom,
    ← cancel_mono ((ιIteration I κ).app f).right, assoc, assoc, assoc, assoc, assoc,
    Iso.inv_hom_id_assoc, πObj_ιIteration_app_right,
    iterationFunctorObjObjRightIso_ιIteration_app_right,
    ← cancel_epi (relativeCellComplexιObjFObjSuccIso I κ f j).hom, Iso.hom_inv_id_assoc]
-- 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 A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift
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 κ
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
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift
have this₁ : HasPushouts.{v, u} C
Tactic: haveI := hasPushouts 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 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
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift
have 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))
Tactic: haveI := preservesColimit I κ i hi _ (relativeCellComplexιObj I κ 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 κ
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
⊢ sq.HasLift
have 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
Tactic: obtain ⟨j, t, ht⟩ := Types.jointly_surjective _
    (isColimitOfPreserves (coyoneda.obj (Opposite.op A))
      (relativeCellComplexιObj I κ f).isColimit) g
-- 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 κ
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
⊢ (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) =
    Iso.hom
        (Iso.refl
          ((TransfiniteCompositionOfShape.F (Y := obj I κ f)
                (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
                  (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).obj
            j)) ≫
      ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom
have dsimp : (TransfiniteCompositionOfShape.F (Y := obj I κ f)
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).map
      (homOfLE sorry) ≫
    Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) =
  𝟙
      ((TransfiniteCompositionOfShape.F (Y := obj I κ f)
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).obj
        j) ≫
    ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom
Tactic: dsimp
-- 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 κ
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
⊢ (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) =
    𝟙
        ((TransfiniteCompositionOfShape.F (Y := obj I κ f)
              (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
                (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).obj
          j) ≫
      ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom
have rw : (TransfiniteCompositionOfShape.F (Y := obj I κ f)
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).map
      (homOfLE sorry) ≫
    Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) =
  𝟙
      ((TransfiniteCompositionOfShape.F (Y := obj I κ f)
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f))).obj
        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 sorry) ≫
      Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j)
Tactic: rw [ιFunctorObj_eq, id_comp]