awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
neg :
  ∀ (a : α)
    (hi :
      ¬IsMax.{w} (α := J)
          ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a : J)),
    (∀
        (hi₀ :
          (s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a =
            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
              ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a) =
            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 ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by
        simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)

Premises used: Iff.mpr, PrincipalSeg.mem_range_iff_rel, 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
a : α
hi :
  ¬IsMax.{w} (α := J)
      ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a : J)
h :
  ∀
    (hi₀ :
      (s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a =
        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 ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a) =
    s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
b : α
rw :
  LE.le.{w} (α := J)
    ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) b : J)
    ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a : J)
⊢ b ≤ a

Tactic:
rw [← s.le_iff_le]

Premises used: PrincipalSeg.le_iff_le
-- 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
a : α
hi :
  ¬IsMax.{w} (α := J)
      ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a : J)
h :
  ∀
    (hi₀ :
      (s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a =
        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 ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a) =
    s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
b : α
⊢ LT.lt.{w} (α := J)
    ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) b : J)
    (Order.succ ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a) :
      J)

Tactic:
simpa only [hi₀] using s.lt_top b

Premises used: PrincipalSeg.lt_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
a : α
hi :
  ¬IsMax.{w} (α := J)
      ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a : J)
h :
  ∀
    (hi₀ :
      (s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a =
        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 ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a) =
    s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
b : α
⊢ LE.le.{w} (α := J)
    ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) b : J)
    ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a : J)

Tactic:
exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b)

Premises used: Order.le_of_lt_succ
-- 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
a : α
hi :
  ¬IsMax.{w} (α := J)
      ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a : J)
h :
  ∀
    (hi₀ :
      (s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a =
        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 ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a) =
    s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
neg : ∀ (this : OrderTop α), HasColimitsOfShape.{u_1, u_1, v, u} α C
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C

Tactic:
have : OrderTop α :=
        { top := a
          le_top b := by
            rw [← s.le_iff_le]
            exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }
-- 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
a : α
hi :
  ¬IsMax.{w} (α := J)
      ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a : J)
h :
  ∀
    (hi₀ :
      (s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a =
        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 ((s.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2) : (a : α) → J) a) =
    s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
this : OrderTop α
⊢ HasColimitsOfShape.{u_1, u_1, 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
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 : Order.IsSuccLimit i
h :
  ∀ b < i,
    ∀ (hi₀ : b = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)),
      HasColimitsOfShape.{u_1, u_1, v, u} α C
hi₀ : i = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
⊢ Order.IsSuccLimit (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
i : J
hi : Order.IsSuccLimit i
h :
  ∀ b < i,
    ∀ (hi₀ : b = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)),
      HasColimitsOfShape.{u_1, u_1, v, u} α C
hi₀ : i = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
hi₁ : Order.IsSuccLimit (s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
⊢ ∀ b < s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2),
    ∀ (hi₀ : b = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)),
      HasColimitsOfShape.{u_1, u_1, v, u} α C

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 : Order.IsSuccLimit (s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
h :
  ∀ b < s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2),
    ∀ (hi₀ : b = 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:
hasColimitsOfShape_of_isSuccLimit' C s hi

Premises used: CategoryTheory.Limits.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
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 : Order.IsSuccLimit (s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
h :
  ∀ b < s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2),
    ∀ (hi₀ : b = 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:
exact hasColimitsOfShape_of_isSuccLimit' C s hi

Premises used: CategoryTheory.Limits.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
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₀ : i = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)
neg :
  ∀ (i : J) (hi : IsMin i) (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
neg₁ :
  ∀ (i : J) (hi : ¬IsMax i),
    (∀ (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)),
        HasColimitsOfShape.{u_1, u_1, v, u} α C
neg₂ :
  ∀ (i : J) (hi : Order.IsSuccLimit i),
    (∀ b < i,
        ∀ (hi₀ : b = s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2)),
          HasColimitsOfShape.{u_1, u_1, v, u} α C) →
      ∀ (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:
induction i using SuccOrder.limitRecOn with
    | isMin i hi =>
      subst hi₀
      exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim
    | succ i hi _ =>
      obtain ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by
        simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)
      have : OrderTop α :=
        { top := a
          le_top b := by
            rw [← s.le_iff_le]
            exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }
      infer_instance
    | isSuccLimit i hi =>
      subst hi₀
      exact hasColimitsOfShape_of_isSuccLimit' C s hi

Premises used: Iff.mpr, PrincipalSeg.mem_range_iff_rel, 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 : LinearOrder α
h : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
j : α
hj : Order.IsSuccLimit j
⊢ Nonempty.{u_1 + 1} (↑(Set.Iio j) : Type u_1)

Tactic:
have := hj.nonempty_Iio.to_subtype
-- 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 : LinearOrder α
h : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
j : α
hj : Order.IsSuccLimit j
this : Nonempty.{u_1 + 1} (↑(Set.Iio j) : Type u_1)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} (↑(Set.Iio j) : Type u_1) C

Tactic:
hasColimitsOfShape_of_initialSeg _
      (InitialSeg.trans (Set.principalSegIio j) h)

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_initialSeg, InitialSeg.trans
-- 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 : LinearOrder α
h : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_6 : Nonempty α
j : α
hj : Order.IsSuccLimit j
this : Nonempty.{u_1 + 1} (↑(Set.Iio j) : Type u_1)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} (↑(Set.Iio j) : Type u_1) C

Tactic:
exact hasColimitsOfShape_of_initialSeg _
      (InitialSeg.trans (Set.principalSegIio j) h)

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_initialSeg, InitialSeg.trans
-- 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
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
j : J
⊢ HasIterationOfShape.{w, v, u} (↑(Set.Iic j) : Type w) C

Tactic:
hasIterationOfShape_of_initialSeg C (Set.initialSegIic j)

Premises used: Set.initialSegIic, CategoryTheory.Limits.hasIterationOfShape_of_initialSeg
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f_1 : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
C : Type u_3
inst_2 : Category.{v_1, u_3} C
F : CategoryTheory.Functor.{u_2, v_1, u_2, u_3} β C
i j : α
f : i ⟶ j
dsimp :
  F.map (⋯.functor.map f) ≫ F.map (homOfLE ⋯) =
    F.map (homOfLE ⋯) ≫ 𝟙 (F.obj (f_1.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)))
⊢ (⋯.functor ⋙ F).map f ≫ F.map (homOfLE ⋯) =
    F.map (homOfLE ⋯) ≫
      CategoryTheory.Functor.map
        (Functor.obj (Functor.const α)
          (F.obj (f_1.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2))))
        f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f_1 : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
C : Type u_3
inst_2 : Category.{v_1, u_3} C
F : CategoryTheory.Functor.{u_2, v_1, u_2, u_3} β C
i j : α
f : i ⟶ j
rw : F.map (⋯.functor.map f ≫ homOfLE ⋯) = F.map (homOfLE ⋯)
⊢ F.map (⋯.functor.map f) ≫ F.map (homOfLE ⋯) =
    F.map (homOfLE ⋯) ≫ 𝟙 (F.obj (f_1.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)))

Tactic:
rw [← F.map_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f_1 : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
C : Type u_3
inst_2 : Category.{v_1, u_3} C
F : CategoryTheory.Functor.{u_2, v_1, u_2, u_3} β C
i j : α
f : i ⟶ j
⊢ F.map (⋯.functor.map f ≫ homOfLE ⋯) = F.map (homOfLE ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
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 : OrderBot J
X Y : C
f : X ⟶ Y
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
F : Functor.{v, v', u, u'} C D
inst_6 : PreservesWellOrderContinuousOfShape J F
inst_7 : PreservesColimitsOfShape J F
⊢ (F.mapIso c.isoBot).inv ≫ (Functor.whiskerRight c.incl F ≫ Iso.hom (Functor.constComp J Y F)).app ⊥ = F.map f

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
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 : OrderBot J
X Y : C
f : X ⟶ Y
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
j : J
i i' : (↑(Set.Iic j) : Type w)
φ : i ⟶ i'
dsimp :
  c.F.map (Functor.map (Monotone.functor (f := (⇑(Set.initialSegIic j) : (a : (↑(Set.Iic j) : Type w)) → J)) ⋯) φ) ≫
      c.F.map (homOfLE ⋯) =
    c.F.map (homOfLE ⋯) ≫ 𝟙 (c.F.obj j)
⊢ Eq (α :=
    Functor.obj (Monotone.functor (f := (⇑(Set.initialSegIic j) : (a : (↑(Set.Iic j) : Type w)) → J)) ⋯ ⋙ c.F) i ⟶
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (↑(Set.Iic j) : Type w)) (c.F.obj j)) i')
    (Functor.map (Monotone.functor (f := (⇑(Set.initialSegIic j) : (a : (↑(Set.Iic j) : Type w)) → J)) ⋯ ⋙ c.F) φ ≫
      c.F.map (homOfLE ⋯))
    (c.F.map (homOfLE ⋯) ≫ Functor.map (Functor.obj (Functor.const (↑(Set.Iic j) : Type w)) (c.F.obj j)) φ)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
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 : OrderBot J
X Y : C
f : X ⟶ Y
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
j : J
i i' : (↑(Set.Iic j) : Type w)
φ : i ⟶ i'
rw :
  c.F.map
      (Functor.map (Monotone.functor (f := (⇑(Set.initialSegIic j) : (a : (↑(Set.Iic j) : Type w)) → J)) ⋯) φ ≫
        homOfLE ⋯) =
    c.F.map (homOfLE ⋯)
⊢ c.F.map (Functor.map (Monotone.functor (f := (⇑(Set.initialSegIic j) : (a : (↑(Set.Iic j) : Type w)) → J)) ⋯) φ) ≫
      c.F.map (homOfLE ⋯) =
    c.F.map (homOfLE ⋯) ≫ 𝟙 (c.F.obj j)

Tactic:
rw [← Functor.map_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
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 : OrderBot J
X Y : C
f : X ⟶ Y
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
j : J
i i' : (↑(Set.Iic j) : Type w)
φ : i ⟶ i'
⊢ c.F.map
      (Functor.map (Monotone.functor (f := (⇑(Set.initialSegIic j) : (a : (↑(Set.Iic j) : Type w)) → J)) ⋯) φ ≫
        homOfLE ⋯) =
    c.F.map (homOfLE ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
F : Functor.{0, v, 0, u} ℕ C
m : ℕ
hm : Order.IsSuccLimit m
⊢ Nonempty (IsColimit (PrincipalSeg.cocone (Set.principalSegIio m) F))

Tactic:
simp at hm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
F : Functor.{w, v, w, u} J C
J' : Type w'
inst_2 : PartialOrder J'
f : InitialSeg (fun (x1 x2 : J') ↦ x1 < x2) fun (x1 x2 : J) ↦ x1 < x2
inst_3 : F.IsWellOrderContinuous
m' : J'
hm' : Order.IsSuccLimit m'
⊢ Order.IsSuccLimit
    ((PrincipalSeg.transInitial (r := fun (x1 x2 : (↑(Set.Iio m') : Type w')) ↦ x1 < x2) (s := fun (x1 x2 : J') ↦
          x1 < x2) (t := fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio m') f).top
      (r := fun (x1 x2 : (↑(Set.Iio m') : Type w')) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))

Tactic:
simpa