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 κ
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
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 ⋯) ≫
      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
⊢ (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

Tactic:
dsimp
-- 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
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
⊢ (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

Tactic:
dsimp
-- 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
rw : i ≫ b = I.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ I.toSet) (Arrow.mk i) hi) ≫ b
⊢ 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

Tactic:
rw [reassoc_of% ht, sq.w]

Premises used: CategoryTheory.CommSq.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 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
⊢ i ≫ b = I.homFamily (Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ I.toSet) (Arrow.mk i) hi) ≫ b

Tactic:
dsimp
-- 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
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
⊢ i ≫
      l ≫
        NatTrans.app
          (TransfiniteCompositionOfShape.incl
            (RelativeCellComplex.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
              (↑I.toSet : Type (max u v))) (relativeCellComplexιObj I κ f)))
          (Order.succ j) =
    g

Tactic:
simp [reassoc_of% hl₁, ← ht]
-- 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
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
rw₁ rw₂ : b = 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

Tactic:
rw [assoc, hl₂]

Premises used: CategoryTheory.Category.assoc
-- 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
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
⊢ sq.HasLift

Tactic:
exact ⟨⟨{
    l := l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j)
    fac_left := by simp [reassoc_of% hl₁, ← ht]
    fac_right := by rw [assoc, hl₂]
  }⟩⟩
-- 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
⊢ I.rlp (X := obj I κ f) (πObj I κ f)

Tactic:
fun _ _ _ hi ↦ hasRightLiftingProperty_πObj _ _ _ hi _

Premises used: CategoryTheory.SmallObject.hasRightLiftingProperty_πObj, CategoryTheory.MorphismProperty.rlp
-- 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
simp : Arrow.Hom.left (𝟙 ((iteration I κ).obj f)) = 𝟙 (obj I κ f.hom)
⊢ objMap I κ (𝟙 f) = 𝟙 (obj I κ f.hom)

Tactic:
simp only [objMap, Functor.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.SmallObject.objMap
-- 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
⊢ Arrow.Hom.left (𝟙 ((iteration I κ).obj f)) = 𝟙 (obj I κ f.hom)

Tactic:
rfl
-- 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 g h : Arrow.{v, u} C
φ : f ⟶ g
ψ : g ⟶ h
simp :
  Arrow.Hom.left ((iteration I κ).map φ ≫ (iteration I κ).map ψ) =
    Arrow.Hom.left ((iteration I κ).map φ) ≫ Arrow.Hom.left ((iteration I κ).map ψ)
⊢ Eq (α := obj I κ f.hom ⟶ obj I κ h.hom) (objMap I κ (φ ≫ ψ)) (objMap I κ φ ≫ objMap I κ ψ)

Tactic:
simp only [objMap, Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.SmallObject.objMap
-- 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 g h : Arrow.{v, u} C
φ : f ⟶ g
ψ : g ⟶ h
⊢ Arrow.Hom.left ((iteration I κ).map φ ≫ (iteration I κ).map ψ) =
    Arrow.Hom.left ((iteration I κ).map φ) ≫ Arrow.Hom.left ((iteration I κ).map ψ)

Tactic:
rfl
-- 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 g : Arrow.{v, u} C
φ : f ⟶ g
⊢ Eq (α := f.left ⟶ obj I κ g.hom) (ιObj I κ f.hom ≫ objMap I κ φ) (Arrow.Hom.left φ ≫ ιObj I κ g.hom)

Tactic:
Arrow.leftFunc.congr_map ((ιIteration I κ).naturality φ).symm

Premises used: CategoryTheory.SmallObject.ιIteration, CategoryTheory.SmallObject.ιObj, CategoryTheory.SmallObject.obj, CategoryTheory.Functor.id, CategoryTheory.Arrow.leftFunc, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.congr_map, CategoryTheory.Arrow, CategoryTheory.SmallObject.objMap, CategoryTheory.Arrow.mk, Eq.symm
-- 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 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)))
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 φ
⊢ Eq (α := obj I κ f.hom ⟶ g.right) (objMap I κ φ ≫ πObj I κ g.hom) (πObj I κ f.hom ≫ Arrow.Hom.right φ)

Tactic:
change _ ≫ _ ≫ e₂.inv = (_ ≫ e₁.inv) ≫ _

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv
-- 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 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)))
⊢ (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
-- 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 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
⊢ 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 φ)
-- 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 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 φ)
⊢ 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₁

Premises used: CategoryTheory.Category.assoc