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 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 φ)
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:
rw [assoc] at h₁

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 κ
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 φ)
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 φ
⊢ 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:
apply h₁.trans

Premises used: Eq.trans
-- 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 φ)
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 φ)
⊢ (((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:
simp only [← cancel_mono e₂.hom, assoc, e₂.inv_hom_id, h₂, e₁.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_assoc, 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 κ
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 φ)
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 φ)
⊢ ((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]

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 κ
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 φ)

Tactic:
apply comp_id

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 κ
⊢ I.rlp.llp = (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts

Tactic:
le_antisymm ?_
    (retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp I κ.ord.ToType)

Premises used: Cardinal.ord, le_antisymm, CategoryTheory.MorphismProperty.retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, 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 κ
refine : I.rlp.llp ≤ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts
⊢ 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)

Premises used: Cardinal.ord, le_antisymm, CategoryTheory.MorphismProperty.retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, 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
hf : I.rlp.llp f
⊢ CategoryStruct.comp (Y := obj I κ f) (ιObj I κ f) (πObj I κ f) = f ≫ 𝟙 Y

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
hf : I.rlp.llp f
⊢ 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⟩
-- 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
hf : I.rlp.llp f
sq : CommSq (X := obj I κ f) (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
⊢ HasLiftingProperty (X := obj I κ f) f (πObj I κ f)

Tactic:
have := hf _ (rlp_π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 : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (X := obj I κ f) (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty (X := obj I κ f) f (πObj I κ f)
⊢ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts f

Tactic:
⟨_, _, _, ?_, transfiniteCompositionsOfShape_ιObj I κ f⟩

Premises used: CategoryTheory.MorphismProperty.retracts, Exists.intro, 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
hf : I.rlp.llp f
sq : CommSq (X := obj I κ f) (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty (X := obj I κ f) f (πObj I κ f)
refine : RetractArrow (W := obj I κ f) f (ιObj I κ f)
⊢ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts f

Tactic:
refine ⟨_, _, _, ?_, transfiniteCompositionsOfShape_ι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 : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (X := obj I κ f) (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty (X := obj I κ f) f (πObj I κ f)
⊢ RetractArrow (W := obj I κ f) f (ιObj I κ f)

Tactic:
exact
    { i := Arrow.homMk (𝟙 _) sq.lift
      r := Arrow.homMk (𝟙 _) (πObj I κ f) }
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.IsCardinalForSmallObjectArgument Cardinal.aleph0
⊢ Nonempty.{w + 1} ((fun (x1 x2 : ULift.{w, 0} ℕ) ↦ x1 < x2) ≃r fun (x1 x2 : Cardinal.aleph0.ord.ToType) ↦ x1 < x2)

Tactic:
simp [← Ordinal.type_eq]

Premises used: Ordinal.type_eq
-- Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.IsCardinalForSmallObjectArgument Cardinal.aleph0
e : ℕ ≃o Cardinal.aleph0.ord.ToType := OrderIso.trans (OrderIso.symm ULift.orderIso.{w, 0}) (OrderIso.ofRelIsoLT ⋯.some)
rw :
  (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts Cardinal.aleph0.ord.ToType).retracts =
    ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts
rw₁ rw₂ :
  (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts Cardinal.aleph0.ord.ToType).retracts =
    (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts Cardinal.aleph0.ord.ToType).retracts
⊢ I.rlp.llp = ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
rw [SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument' _ Cardinal.aleph0,
    MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso _ e]

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso, Cardinal.aleph0, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'
-- 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 κ
⊢ I.rlp.llp = (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
le_antisymm ?_
    (retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp I)

Premises used: CategoryTheory.MorphismProperty.retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp, le_antisymm
-- 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 κ
refine : I.rlp.llp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
⊢ I.rlp.llp = (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
refine le_antisymm ?_
    (retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp I)

Premises used: CategoryTheory.MorphismProperty.retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp, le_antisymm
-- 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 κ
rw :
  (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
⊢ I.rlp.llp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
rw [llp_rlp_of_isCardinalForSmallObjectArgument' I κ]

Premises used: CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'
-- 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 κ
a :
  transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType ≤
    transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts
⊢ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
apply retracts_monotone

Premises used: CategoryTheory.MorphismProperty.retracts_monotone
-- 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 κ
⊢ transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType ≤
    transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts

Tactic:
apply transfiniteCompositionsOfShape_le_transfiniteCompositions

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i ≤ j
k : J
hk : k < i
⊢ (restrictionLT F hi).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) =
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i ≤ j
k₁ k₂ : (↑(Set.Iio i) : Type w)
φ : k₁ ⟶ k₂
⊢ ⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂

Tactic:
simpa using leOfHom φ

Premises used: CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i ≤ j
k₁ k₂ : (↑(Set.Iio i) : Type w)
φ : k₁ ⟶ k₂
⊢ (restrictionLT F hi).map φ = F.map (homOfLE ⋯)

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i ≤ j
k : J
hk : k ≤ i
⊢ (restrictionLE F hi).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) k hk) =
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i ≤ j
k₁ k₂ : (↑(Set.Iic i) : Type w)
φ : k₁ ⟶ k₂
⊢ ⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂

Tactic:
simpa using leOfHom φ

Premises used: CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i ≤ j
k₁ k₂ : (↑(Set.Iic i) : Type w)
φ : k₁ ⟶ k₂
⊢ (restrictionLE F hi).map φ = F.map (homOfLE ⋯)

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X : C
⊢ Φ.prop (Φ.toSucc X)

Tactic:
⟨_⟩

Premises used: CategoryTheory.MorphismProperty.ofHoms.mk, CategoryTheory.SmallObject.SuccStruct.prop
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
mp : Φ.prop f → Arrow.mk f = Φ.toSuccArrow X
mpr : Arrow.mk f = Φ.toSuccArrow X → Φ.prop f
⊢ Φ.prop f ↔ Arrow.mk f = Φ.toSuccArrow X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X_1 X Y : C
⊢ Arrow.mk (Φ.toSucc X_1) = Φ.toSuccArrow X_1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
mpr : Φ.toSuccArrow X ∈ Φ.prop.toSet
⊢ Φ.prop f

Tactic:
rw [← Φ.prop.arrow_mk_mem_toSet_iff, h]

Premises used: CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff, CategoryTheory.SmallObject.SuccStruct.prop
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.toSuccArrow X ∈ Φ.prop.toSet

Tactic:
apply prop_toSucc

Premises used: CategoryTheory.SmallObject.SuccStruct.prop_toSucc
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
mk : Φ.succ X = Φ.succ X
⊢ Φ.succ X = Y

Tactic:
cases hf
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X : C
⊢ Φ.succ X = Φ.succ X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
mk : Φ.toSucc X = Φ.toSucc X ≫ eqToHom ⋯
⊢ f = Φ.toSucc X ≫ eqToHom ⋯

Tactic:
cases hf
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X : C
⊢ Φ.toSucc X = Φ.toSucc X ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ Iso.hom (Iso.refl (Arrow.mk f).left) ≫ (Φ.toSuccArrow X).hom = (Arrow.mk f).hom ≫ Iso.hom (eqToIso ⋯)

Tactic:
simp [hf.fac]

Premises used: CategoryTheory.SmallObject.SuccStruct.prop.fac
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i ≤ j
⊢ i ≤ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i ≤ j
⊢ arrowMap F i i ⋯ hi = Arrow.mk (𝟙 (F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hi)))

Tactic:
simp [arrowMap]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowMap
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
j' : J
hj' : j' ≤ j
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ ≤ j'
⊢ arrowMap (restrictionLE F hj') i₁ i₂ h₁₂ h₂ = arrowMap F i₁ i₂ h₁₂ ⋯

Tactic:
rfl

Premises used: CategoryTheory.SmallObject.restrictionLE, Set.Mem, setOf, CategoryTheory.Functor.comp, CategoryTheory.homOfLE, CategoryTheory.SmallObject.SuccStruct.arrowMap, Set.Iic, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
F : Functor.{w, v, w, u} (↑(Set.Iic j) : Type w) C
i : J
hi : i < j
⊢ arrowSucc F i hi = arrowMap F i (Order.succ i) ⋯ ⋯

Tactic:
rfl

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowSucc, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : HasIterationOfShape.{w, v, u} J C
i : J
F : Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C
hi : Order.IsSuccLimit i
k : J
hk : k < i
⊢ arrowι F hi k hk =
    Arrow.mk (X := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)) (Y := colimit F)
      (colimit.ι F (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))

Tactic:
rfl

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowι, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : i < j
⊢ iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯) =
    Φ.succ (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))

Tactic:
congr_arg Comma.right (iter.arrowSucc_eq i hi)

Premises used: CategoryTheory.Comma.right, congr_arg, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq