awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd
Goal:
C : Type u_1
I : Type u_2
inst : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst_1 : HasProduct.{u_2, v_1, u_1} X
inst_2 : HasProduct.{u_2, v_1, u_1} Y
inst_3 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ X (↑i : I)
inst_4 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ X (↑i : I)
inst_5 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ Y (↑i : I)
inst_6 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ Y (↑i : I)
inst_7 : (i : I) → Decidable (P i)
⊢ ∀
    (s :
      BinaryFan.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))),
    CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} X)
        ((fun
              (s :
                BinaryFan.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                  (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))) ↦
            (lift fun (b : I) ↦
                if h : P b then
                  CategoryStruct.comp (Y :=
                    Functor.obj.{0, v_1, 0, u_1}
                      (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                      { as := WalkingPair.left : Discrete WalkingPair })
                    (s.π.app { as := WalkingPair.left })
                    (π (fun (i : { x : I // P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ P x) b h))
                else
                  CategoryStruct.comp (Y :=
                    Functor.obj.{0, v_1, 0, u_1}
                      (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                      { as := WalkingPair.right : Discrete WalkingPair })
                    (s.π.app { as := WalkingPair.right })
                    (π (fun (i : { x : I // ¬P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ ¬P x) b h)) :
              s.pt ⟶ piObj.{u_2, v_1, u_1} X))
          s)
        (map' (Subtype.val (p := fun (x : I) ↦ P x)) fun (x : { x : I // P x }) ↦ 𝟙 (X (↑x : I))) =
      s.fst

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd
Goal:
C : Type u_1
I : Type u_2
inst : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst_1 : HasProduct.{u_2, v_1, u_1} X
inst_2 : HasProduct.{u_2, v_1, u_1} Y
inst_3 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ X (↑i : I)
inst_4 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ X (↑i : I)
inst_5 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ Y (↑i : I)
inst_6 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ Y (↑i : I)
inst_7 : (i : I) → Decidable (P i)
⊢ ∀
    (s :
      BinaryFan.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))),
    CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} X)
        ((fun
              (s :
                BinaryFan.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                  (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))) ↦
            (lift fun (b : I) ↦
                if h : P b then
                  CategoryStruct.comp (Y :=
                    Functor.obj.{0, v_1, 0, u_1}
                      (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                      { as := WalkingPair.left : Discrete WalkingPair })
                    (s.π.app { as := WalkingPair.left })
                    (π (fun (i : { x : I // P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ P x) b h))
                else
                  CategoryStruct.comp (Y :=
                    Functor.obj.{0, v_1, 0, u_1}
                      (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                      { as := WalkingPair.right : Discrete WalkingPair })
                    (s.π.app { as := WalkingPair.right })
                    (π (fun (i : { x : I // ¬P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ ¬P x) b h)) :
              s.pt ⟶ piObj.{u_2, v_1, u_1} X))
          s)
        (map' (Subtype.val (p := fun (x : I) ↦ ¬P x)) fun (x : { x : I // ¬P x }) ↦ 𝟙 (X (↑x : I))) =
      s.snd

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd
Goal:
C : Type u_1
I : Type u_2
inst : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst_1 : HasProduct.{u_2, v_1, u_1} X
inst_2 : HasProduct.{u_2, v_1, u_1} Y
inst_3 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ X (↑i : I)
inst_4 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ X (↑i : I)
inst_5 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ Y (↑i : I)
inst_6 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ Y (↑i : I)
inst_7 : (i : I) → Decidable (P i)
x :
  BinaryFan.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
    (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))
x_1 : x.pt ⟶ piObj.{u_2, v_1, u_1} X
h₁ : (x_1 ≫ map' (Subtype.val (p := fun (x : I) ↦ P x)) fun (x : { x : I // P x }) ↦ 𝟙 (X (↑x : I))) = x.fst
h₂ : (x_1 ≫ map' (Subtype.val (p := fun (x : I) ↦ ¬P x)) fun (x : { x : I // ¬P x }) ↦ 𝟙 (X (↑x : I))) = x.snd
b : I
h : P b
⊢ x_1 ≫ π X b =
    CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} X)
      ((fun
            (s :
              BinaryFan.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))) ↦
          (lift fun (b : I) ↦
              if h : P b then
                CategoryStruct.comp (Y :=
                  Functor.obj.{0, v_1, 0, u_1}
                    (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                      (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                    { as := WalkingPair.left : Discrete WalkingPair })
                  (s.π.app { as := WalkingPair.left })
                  (π (fun (i : { x : I // P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ P x) b h))
              else
                CategoryStruct.comp (Y :=
                  Functor.obj.{0, v_1, 0, u_1}
                    (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                      (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                    { as := WalkingPair.right : Discrete WalkingPair })
                  (s.π.app { as := WalkingPair.right })
                  (π (fun (i : { x : I // ¬P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ ¬P x) b h)) :
            s.pt ⟶ piObj.{u_2, v_1, u_1} X))
        x)
      (π X b)

Tactic:
simp [← h₁, dif_pos h]

Premises used: dif_pos
-- Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd
Goal:
C : Type u_1
I : Type u_2
inst : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst_1 : HasProduct.{u_2, v_1, u_1} X
inst_2 : HasProduct.{u_2, v_1, u_1} Y
inst_3 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ X (↑i : I)
inst_4 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ X (↑i : I)
inst_5 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ Y (↑i : I)
inst_6 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ Y (↑i : I)
inst_7 : (i : I) → Decidable (P i)
x :
  BinaryFan.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
    (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))
x_1 : x.pt ⟶ piObj.{u_2, v_1, u_1} X
h₁ : (x_1 ≫ map' (Subtype.val (p := fun (x : I) ↦ P x)) fun (x : { x : I // P x }) ↦ 𝟙 (X (↑x : I))) = x.fst
h₂ : (x_1 ≫ map' (Subtype.val (p := fun (x : I) ↦ ¬P x)) fun (x : { x : I // ¬P x }) ↦ 𝟙 (X (↑x : I))) = x.snd
b : I
h : ¬P b
⊢ x_1 ≫ π X b =
    CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} X)
      ((fun
            (s :
              BinaryFan.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))) ↦
          (lift fun (b : I) ↦
              if h : P b then
                CategoryStruct.comp (Y :=
                  Functor.obj.{0, v_1, 0, u_1}
                    (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                      (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                    { as := WalkingPair.left : Discrete WalkingPair })
                  (s.π.app { as := WalkingPair.left })
                  (π (fun (i : { x : I // P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ P x) b h))
              else
                CategoryStruct.comp (Y :=
                  Functor.obj.{0, v_1, 0, u_1}
                    (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                      (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                    { as := WalkingPair.right : Discrete WalkingPair })
                  (s.π.app { as := WalkingPair.right })
                  (π (fun (i : { x : I // ¬P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ ¬P x) b h)) :
            s.pt ⟶ piObj.{u_2, v_1, u_1} X))
        x)
      (π X b)

Tactic:
simp [← h₂, dif_neg h]

Premises used: dif_neg
-- Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd
Goal:
C : Type u_1
I : Type u_2
inst : Category.{v_1, u_1} C
X : I → C
P : I → Prop
inst_1 : HasProduct.{u_2, v_1, u_1} X
inst_2 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ X (↑i : I)
inst_3 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ X (↑i : I)
⊢ HasBinaryProduct.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
    (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))

Tactic:
⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩

Premises used: CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit, CategoryTheory.Limits.Pi.binaryFanOfProp, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd
Goal:
C : Type u_1
I : Type u_2
inst : Category.{v_1, u_1} C
X : I → C
P : I → Prop
inst_1 : HasProduct.{u_2, v_1, u_1} X
inst_2 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ X (↑i : I)
inst_3 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ X (↑i : I)
⊢ HasBinaryProduct.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
    (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))

Tactic:
exact ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd
Goal:
C : Type u_1
I : Type u_2
inst : Category.{v_1, u_1} C
X : I → C
P : I → Prop
inst_1 : HasProduct.{u_2, v_1, u_1} X
inst_2 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ X (↑i : I)
inst_3 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ X (↑i : I)
⊢ HasBinaryProduct.{v_1, u_1} (C := C) (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
    (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))

Tactic:
classical exact ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Preorder J
inst_2 : OrderBot J
x : CategoryTheory.Functor.{w, v, w, u} J C
⊢ HasLimit x

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Preorder J
inst_2 : OrderTop J
x : CategoryTheory.Functor.{w, v, w, u} J C
⊢ HasColimit x

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C

Tactic:
HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit j hj

Premises used: CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
α : Type u_1
inst_3 : PartialOrder α
h : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
hα : Order.IsSuccLimit (h.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
⊢ HasColimitsOfShape.{w, w, v, u}
    (↑(Set.Iio (h.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))) : Type w) C

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C h.top hα
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
α : Type u_1
inst_3 : PartialOrder α
h : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
hα : Order.IsSuccLimit (h.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
this :
  HasColimitsOfShape.{w, w, v, u}
    (↑(Set.Iio (h.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))) : Type w) C
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
hasColimitsOfShape_of_equivalence h.orderIsoIio.equivalence.symm

Premises used: OrderIso.equivalence, PrincipalSeg.orderIsoIio, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
α : Type u_1
inst_3 : PartialOrder α
h : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
hα : Order.IsSuccLimit (h.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
this :
  HasColimitsOfShape.{w, w, v, u}
    (↑(Set.Iio (h.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))) : Type w) C
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
exact hasColimitsOfShape_of_equivalence h.orderIsoIio.equivalence.symm

Premises used: OrderIso.equivalence, PrincipalSeg.orderIsoIio, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C j hj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
⊢ HasColimitsOfShape (↑(Set.Iio j) : Type w) (Arrow.{v, u} C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
⊢ HasColimitsOfShape (↑(Set.Iio j) : Type w) (Functor.{v', v, u', u} K C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
pos :
  ∀ (hf : Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)),
    HasColimitsOfShape.{u_1, u_1, v, u} α C
neg :
  ∀ (hf : ¬Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)),
    HasColimitsOfShape.{u_1, u_1, v, u} α C
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
by_cases hf : Function.Surjective f

Premises used: DFunLike.coe, Function.Surjective
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
hf : Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
hasColimitsOfShape_of_equivalence
      (OrderIso.ofRelIsoLT (RelIso.ofSurjective f.toRelEmbedding hf)).equivalence.symm

Premises used: OrderIso.equivalence, OrderIso.ofRelIsoLT, InitialSeg.toRelEmbedding, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, RelIso.ofSurjective, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
hf : Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
exact hasColimitsOfShape_of_equivalence
      (OrderIso.ofRelIsoLT (RelIso.ofSurjective f.toRelEmbedding hf)).equivalence.symm

Premises used: OrderIso.equivalence, OrderIso.ofRelIsoLT, InitialSeg.toRelEmbedding, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, RelIso.ofSurjective, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
hf : ¬Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)
s : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2 :=
  f.toPrincipalSeg (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) hf
⊢ ∃ (i : J), i = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
hf : ¬Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)
s : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2 :=
  f.toPrincipalSeg (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) hf
neg :
  ∀ (i : J) (hi₀ : i = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)),
    HasColimitsOfShape.{u_1, u_1, v, u} α C
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
obtain ⟨i, hi₀⟩ : ∃ i, i = s.top := ⟨_, rfl⟩

Premises used: PrincipalSeg.top
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
hf : ¬Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)
s : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2 :=
  f.toPrincipalSeg (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) hf
i : J
hi : IsMin i
hi₀ : i = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
⊢ IsMin (s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))

Tactic:
subst hi₀
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
hf : ¬Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)
s : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2 :=
  f.toPrincipalSeg (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) hf
hi : IsMin (s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
(hi.not_lt (s.lt_top (Classical.arbitrary _))).elim

Premises used: False.elim, PrincipalSeg.lt_top, IsMin.not_lt, Classical.arbitrary
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
hf : ¬Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)
s : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2 :=
  f.toPrincipalSeg (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) hf
hi : IsMin (s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim

Premises used: False.elim, PrincipalSeg.lt_top, IsMin.not_lt, Classical.arbitrary
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
Goal:
J : Type w
inst : LinearOrder J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasIterationOfShape.{w, v, u} J C
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : Type u_1
inst_5 : PartialOrder α
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
hf : ¬Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)
s : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2 :=
  f.toPrincipalSeg (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) hf
i : J
hi : ¬IsMax i
h :
  ∀ (hi₀ : i = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)),
    HasColimitsOfShape.{u_1, u_1, v, u} α C
hi₀ : Order.succ i = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
⊢ i < s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)

Tactic:
simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi

Premises used: Order.lt_succ_of_not_isMax