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 κ
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
⊢ (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.hom (Iso.symm (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j)) =
    Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom
have dsimp : (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) =
  Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f 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
⊢ (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) =
    Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom
have rw : Eq (α :=
  (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) ⟶
    (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).right)
  ((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))
  (Iso.hom (relativeCellComplexιObjFObjSuccIso I κ f j) ≫
    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))
Tactic: rw [πFunctorObj_eq, assoc, Iso.hom_inv_id_assoc]
-- 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
⊢ t ≫
      NatTrans.app
          (TransfiniteCompositionOfShape.incl
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f)))
          j ≫
        πObj I κ f =
    I.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ I.toSet) (Arrow.mk i) hi) ≫ b
have rw : i ≫ b = I.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ I.toSet) (Arrow.mk i) hi) ≫ b
Tactic: rw [reassoc_of% ht, sq.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 κ
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
⊢ sq.HasLift
have 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 sorry))
  (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
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)
-- 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
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 ≫ 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
rw :
  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
⊢ (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
have rw₁ : b = b
Tactic: rw [assoc, hl₂]
-- 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
⊢ objMap I κ (𝟙 f) = 𝟙 (obj I κ f.hom)
have simp : Arrow.Hom.left (𝟙 ((iteration I κ).obj f)) = 𝟙 (obj I κ f.hom)
Tactic: simp only [objMap, Functor.map_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 g h : Arrow.{v, u} C
φ : f ⟶ g
ψ : g ⟶ h
⊢ Eq (α := obj I κ f.hom ⟶ obj I κ h.hom) (objMap I κ (φ ≫ ψ)) (objMap I κ φ ≫ objMap I κ ψ)
have simp : Arrow.Hom.left ((iteration I κ).map φ ≫ (iteration I κ).map ψ) =
  Arrow.Hom.left ((iteration I κ).map φ) ≫ Arrow.Hom.left ((iteration I κ).map ψ)
Tactic: simp only [objMap, Functor.map_comp]
-- 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 g : Arrow.{v, u} C
φ : f ⟶ g
e₁ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk f.hom)))
e₂ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk g.hom)))
⊢ Eq (α := obj I κ f.hom ⟶ g.right) (objMap I κ φ ≫ πObj I κ g.hom) (πObj I κ f.hom ≫ Arrow.Hom.right φ)
have change : objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
  (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ
Tactic: change _ ≫ _ ≫ e₂.inv = (_ ≫ e₁.inv) ≫ _
-- 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 g : Arrow.{v, u} C
φ : f ⟶ g
e₁ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk f.hom)))
e₂ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk g.hom)))
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ
have h₁ : (Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom) ≫ e₂.inv =
  (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
Tactic: have h₁ := ((iteration I κ).map φ).w =≫ e₂.inv
-- 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 g : Arrow.{v, u} C
φ : f ⟶ g
e₁ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk f.hom)))
e₂ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk g.hom)))
h₁ :
  (Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom) ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ
have h₂ : Arrow.Hom.right φ ≫ e₂.hom = e₁.hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
Tactic: have h₂ : φ.right ≫ e₂.hom = e₁.hom ≫ ((iteration I κ).map φ).right :=
    ((Functor.whiskerRight (ιIteration I κ) Arrow.rightFunc).naturality φ)
-- 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 g : Arrow.{v, u} C
φ : f ⟶ g
e₁ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk f.hom)))
e₂ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk g.hom)))
h₁ :
  (Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom) ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
h₂ : Arrow.Hom.right φ ≫ e₂.hom = e₁.hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ
have h₃ : Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom ≫ e₂.inv =
  (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
Tactic: rw [assoc] at h₁
Cleared hypotheses: h₁, 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 κ
f g : Arrow.{v, u} C
φ : f ⟶ g
e₁ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk f.hom)))
e₂ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk g.hom)))
h₁ :
  Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
h₂ : Arrow.Hom.right φ ≫ e₂.hom = e₁.hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ
have apply : (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv =
  (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ
Tactic: apply h₁.trans
-- 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 g : Arrow.{v, u} C
φ : f ⟶ g
e₁ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk f.hom)))
e₂ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk g.hom)))
h₁ :
  Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
h₂ : Arrow.Hom.right φ ≫ e₂.hom = e₁.hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
⊢ (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ
have simp : ((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ) ≫ 𝟙 ((iteration I κ).obj (Arrow.mk g.hom)).right =
  ((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
Tactic: simp only [← cancel_mono e₂.hom, assoc, e₂.inv_hom_id, h₂, e₁.inv_hom_id_assoc]
-- 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 g : Arrow.{v, u} C
φ : f ⟶ g
e₁ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk f.hom)))
e₂ : (Functor.obj (𝟭 (Arrow.{v, u} C)) (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right (NatTrans.app (ιIteration I κ) (Arrow.mk g.hom)))
h₁ :
  Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
h₂ : Arrow.Hom.right φ ≫ e₂.hom = e₁.hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
⊢ ((iteration I κ).obj f).hom ≫
      Arrow.Hom.right ((iteration I κ).map φ) ≫ 𝟙 ((iteration I κ).obj (Arrow.mk g.hom)).right =
    ((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
have rw : (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫
    𝟙 ((iteration I κ).obj (Arrow.mk g.hom)).right =
  ((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
Tactic: rw [← assoc]
-- 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 κ
⊢ I.rlp.llp = (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts
have refine : I.rlp.llp ≤ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts
Tactic: refine le_antisymm ?_
    (retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp I κ.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
hf : I.rlp.llp f
⊢ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts f
have sq : CommSq (X := obj I κ f) (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
Tactic: have sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 _) := ⟨by simp⟩