awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
J' : Type w'
inst_5 : LinearOrder J'
inst_6 : SuccOrder J'
inst_7 : OrderBot J'
inst_8 : WellFoundedLT J'
e : J ≃o J'
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W.transfiniteCompositionsOfShape J f ↔ W.transfiniteCompositionsOfShape J' f
⊢ W.transfiniteCompositionsOfShape J = W.transfiniteCompositionsOfShape J'

Tactic:
ext _ _ f
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
J' : Type w'
inst_5 : LinearOrder J'
inst_6 : SuccOrder J'
inst_7 : OrderBot J'
inst_8 : WellFoundedLT J'
e : J ≃o J'
X Y : C
f : X ⟶ Y
⊢ W.transfiniteCompositionsOfShape J f ↔ W.transfiniteCompositionsOfShape J' f

Tactic:
⟨fun ⟨h⟩ ↦ ⟨h.ofOrderIso e.symm⟩, fun ⟨h⟩ ↦ ⟨h.ofOrderIso e⟩⟩

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape, _private.0.CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso.match_1, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofOrderIso, Nonempty.intro, OrderIso.symm, Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
J' : Type w'
inst_5 : LinearOrder J'
inst_6 : SuccOrder J'
inst_7 : OrderBot J'
inst_8 : WellFoundedLT J'
e : J ≃o J'
X Y : C
f : X ⟶ Y
⊢ W.transfiniteCompositionsOfShape J f ↔ W.transfiniteCompositionsOfShape J' f

Tactic:
exact ⟨fun ⟨h⟩ ↦ ⟨h.ofOrderIso e.symm⟩, fun ⟨h⟩ ↦ ⟨h.ofOrderIso e⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
J' : Type w'
inst_6 : LinearOrder J'
inst_7 : SuccOrder J'
inst_8 : OrderBot J'
inst_9 : WellFoundedLT J'
⊢ (W.transfiniteCompositionsOfShape J).RespectsIso

Tactic:
RespectsIso.of_respects_arrow_iso _ (fun _ _ e ⟨h⟩ ↦ ⟨h.ofArrowIso e⟩)

Premises used: _private.0.CategoryTheory.MorphismProperty.instRespectsIsoTransfiniteCompositionsOfShape.match_1, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape, CategoryTheory.Arrow.hom, CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso, Nonempty.intro, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofArrowIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
⊢ W.transfiniteCompositionsOfShape J f

Tactic:
⟨h⟩

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape, Nonempty.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
G : Functor.{v, v', u, u'} C D
inst_6 : PreservesWellOrderContinuousOfShape J G
X Y : C
f : X ⟶ Y
P : MorphismProperty.{v', u'} D
inst_7 : PreservesColimitsOfShape J G
h : (P.inverseImage G).transfiniteCompositionsOfShape J f
⊢ P.transfiniteCompositionsOfShape J (G.map f)

Tactic:
h.some.map.mem

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem, Nonempty.some, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
inst_5 : W.IsStableUnderTransfiniteCompositionOfShape J
⊢ W.transfiniteCompositionsOfShape J ≤ W

Tactic:
IsStableUnderTransfiniteCompositionOfShape.le

Premises used: CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.le
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
J' : Type w'
inst_5 : LinearOrder J'
inst_6 : SuccOrder J'
inst_7 : OrderBot J'
inst_8 : WellFoundedLT J'
e : J ≃o J'
⊢ W.IsStableUnderTransfiniteCompositionOfShape J ↔ W.IsStableUnderTransfiniteCompositionOfShape J'

Tactic:
simp only [isStableUnderTransfiniteCompositionOfShape_iff,
    W.transfiniteCompositionsOfShape_eq_of_orderIso e]

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso, CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
g : ⊥ ⟶ j
⊢ g = homOfLE ⋯

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
g : ⊥ ⟶ j
obtain :
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (hf.toTransfiniteCompositionOfShape (W := W).F.map g)

Tactic:
obtain rfl : g = homOfLE bot_le := rfl

Premises used: CategoryTheory.homOfLE, bot_le, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : IsMin j
isMin :
  ∀ (hj : IsMin.{w} (α := J) ⊥),
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
obtain rfl := hj.eq_bot

Premises used: IsMin.eq_bot, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
hj : IsMin.{w} (α := J) ⊥
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
simpa using W.id_mem _

Premises used: CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' :
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
succ :
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯) ≫
      hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]

Premises used: CategoryTheory.TransfiniteCompositionOfShape.F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.homOfLE_comp, CategoryTheory.Functor.map_comp, Order.le_succ, bot_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' :
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯) ≫
      hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
W.comp_mem _ _ hj' (hf.map_mem j hj)

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' :
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯) ≫
      hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
exact W.comp_mem _ _ hj' (hf.map_mem j hj)

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : Order.IsSuccLimit j
hj' :
  ∀ b < j,
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj b)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
isSuccLimit :
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
letI : OrderBot (Set.Iio j) :=
      { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
        bot_le j := bot_le }
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : Order.IsSuccLimit j
hj' :
  ∀ b < j,
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj b)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
this : OrderBot (↑(Set.Iio j) : Type w) := { bot := ⟨⊥, ⋯⟩, bot_le := ⋯ }
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le, CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit, PrincipalSeg.monotone, CategoryTheory.Functor.isColimitOfIsWellOrderContinuous, CategoryTheory.TransfiniteCompositionOfShape.F, Monotone.functor, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, Set.principalSegIio, CategoryTheory.Functor.obj, Subtype.property
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : Order.IsSuccLimit j
hj' :
  ∀ b < j,
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj b)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
this : OrderBot (↑(Set.Iio j) : Type w) := { bot := ⟨⊥, ⋯⟩, bot_le := ⋯ }
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
exact MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le, CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit, PrincipalSeg.monotone, CategoryTheory.Functor.isColimitOfIsWellOrderContinuous, CategoryTheory.TransfiniteCompositionOfShape.F, Monotone.functor, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, Set.principalSegIio, CategoryTheory.Functor.obj, Subtype.property
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
isMin :
  ∀ (j : J) (hj : IsMin j),
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj j)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
succ :
  ∀ (j : J) (hj : ¬IsMax j)
    (hj' :
      W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
        hf.toTransfiniteCompositionOfShape (W := W).F.obj j)
        (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))),
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
isSuccLimit :
  ∀ (j : J) (hj : Order.IsSuccLimit j)
    (hj' :
      ∀ b < j,
        W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
          hf.toTransfiniteCompositionOfShape (W := W).F.obj b)
          (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))),
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj j)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))

Tactic:
induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa using W.id_mem _
  | succ j hj hj' =>
    rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]
    exact W.comp_mem _ _ hj' (hf.map_mem j hj)
  | isSuccLimit j hj hj' =>
    letI : OrderBot (Set.Iio j) :=
      { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
        bot_le j := bot_le }
    exact MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))

Premises used: CategoryTheory.TransfiniteCompositionOfShape.F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.homOfLE_comp, CategoryTheory.Functor.map_comp, Order.le_succ, CategoryTheory.MorphismProperty.id_mem, bot_le, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_7 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
inst_6 : W.RespectsIso
⊢ W f

Tactic:
(MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk hf.isoBot.symm (Iso.refl _))).2
    (MorphismProperty.colimitsOfShape_le _
      (.of_isColimit hf.isColimit (fun j ↦ mem_map_bot_le _ hJ _)))

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.colimitsOfShape_le, CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit, CategoryTheory.Iso.refl, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape.mem_map_bot_le, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.homOfLE, CategoryTheory.Iso.symm, CategoryTheory.TransfiniteCompositionOfShape.isoBot, CategoryTheory.TransfiniteCompositionOfShape.isColimit, bot_le, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
inst_6 : W.IsMultiplicative
inst_7 : W.RespectsIso
inst_8 : IsStableUnderFilteredColimits.{w, w, v, u} W
x : Type w
x_1 : LinearOrder x
x_2 : SuccOrder x
x_3 : OrderBot x
h : WellFoundedLT x
⊢ W.IsStableUnderColimitsOfShape x

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
⊢ IsStableUnderTransfiniteComposition.{u_1, v, u} (isomorphisms C)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
inst_2 : UnivLE.{w, w'}
J : Type w
x : LinearOrder J
x_1 : SuccOrder J
x_2 : OrderBot J
h : WellFoundedLT J
rw : IsStableUnderTransfiniteCompositionOfShape.{w', v, u} W (Shrink.{w', w} J)
⊢ W.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
rw [isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso W
      (orderIsoShrink.{w'} J)]
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
inst_2 : UnivLE.{w, w'}
J : Type w
x : LinearOrder J
x_1 : SuccOrder J
x_2 : OrderBot J
h : WellFoundedLT J
⊢ IsStableUnderTransfiniteCompositionOfShape.{w', v, u} W (Shrink.{w', w} J)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
⊢ W.IsStableUnderTransfiniteComposition

Tactic:
shrink.{0, w'} W

Premises used: CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.shrink
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
⊢ transfiniteCompositions.{w, v, u} W f ↔
    ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
      W.transfiniteCompositionsOfShape J f

Tactic:
simp only [transfiniteCompositions, iSup_iff]

Premises used: CategoryTheory.MorphismProperty.iSup_iff, CategoryTheory.MorphismProperty.transfiniteCompositions
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
rw :
  ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W f

Tactic:
rw [transfiniteCompositions_iff]

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositions_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f

Tactic:
⟨_, _, _, _, _, hf⟩

Premises used: Exists.intro