awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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 α
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have pos : ∀ (hf : Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)),
  HasColimitsOfShape.{u_1, u_1, v, u} α C
Tactic: by_cases hf : Function.Surjective f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have neg : ∀ (hf : ¬Function.Surjective.{u_1 + 1, w + 1} (α := α) (β := J) (⇑f : (a : α) → J)),
  HasColimitsOfShape.{u_1, u_1, v, u} α C
Tactic: by_cases hf : Function.Surjective f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have 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
Tactic: obtain ⟨i, hi₀⟩ : ∃ i, i = s.top := ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (hypothesis)
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)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have hi₁ : IsMin (s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
Tactic: subst hi₀
Cleared hypotheses: i, hi, hi₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have 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
Tactic: obtain ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by
        simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)
Cleared hypotheses: i, hi, h, hi₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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 : α
⊢ b ≤ a
have 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)
Tactic: rw [← s.le_iff_le]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have neg : ∀ (this : OrderTop α), 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) }
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (hypothesis)
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)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have hi₁ : Order.IsSuccLimit (s.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦ x1 < x2))
Tactic: subst hi₀
Cleared hypotheses: i, hi, h, hi₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (hypothesis)
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))
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have a : ∀ 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₀
Cleared hypotheses: i, hi, h, hi₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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)
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have 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
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
Cleared hypotheses: i, hi₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have 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
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
Cleared hypotheses: i, hi₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (goal)
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
⊢ HasColimitsOfShape.{u_1, u_1, v, u} α C
have 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
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
Cleared hypotheses: i, hi₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape (hypothesis)
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
⊢ HasColimitsOfShape.{u_1, u_1, v, u} (↑(Set.Iio j) : Type u_1) C
have this : Nonempty.{u_1 + 1} (↑(Set.Iio j) : Type u_1)
Tactic: have := hj.nonempty_Iio.to_subtype
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg (goal)
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
⊢ (⋯.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
have dsimp : F.map (sorry.functor.map f) ≫ F.map (homOfLE sorry) =
  F.map (homOfLE sorry) ≫ 𝟙 (F.obj (f_1.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg (goal)
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) ≫ F.map (homOfLE ⋯) =
    F.map (homOfLE ⋯) ≫ 𝟙 (F.obj (f_1.top (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)))
have rw : F.map (sorry.functor.map f ≫ homOfLE sorry) = F.map (homOfLE sorry)
Tactic: rw [← F.map_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape (goal)
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'
⊢ 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)) φ)
have dsimp : c.F.map (Functor.map (Monotone.functor (f := (⇑(Set.initialSegIic j) : (a : (↑(Set.Iic j) : Type w)) → J)) sorry) φ) ≫
    c.F.map (homOfLE sorry) =
  c.F.map (homOfLE sorry) ≫ 𝟙 (c.F.obj j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape (goal)
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)) ⋯) φ) ≫
      c.F.map (homOfLE ⋯) =
    c.F.map (homOfLE ⋯) ≫ 𝟙 (c.F.obj j)
have rw : c.F.map
    (Functor.map (Monotone.functor (f := (⇑(Set.initialSegIic j) : (a : (↑(Set.Iic j) : Type w)) → J)) sorry) φ ≫
      homOfLE sorry) =
  c.F.map (homOfLE sorry)
Tactic: rw [← Functor.map_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
⊢ IsColimit.{w, v, w, u} (J := (↑(Set.Iio m) : Type w)) (C := C) (F :=
    comp (D := { x : J // x ∈ Set.Ici j })
      (Monotone.functor (f :=
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s :=
              fun (x1 x2 : { x : J // x ∈ Set.Ici j }) ↦ x1 < x2) (Set.principalSegIio m)) :
          (a : (↑(Set.Iio m) : Type w)) → { x : J // x ∈ Set.Ici j }))
        ⋯)
      (Monotone.functor ⋯ ⋙ F))
    (PrincipalSeg.cocone (Set.principalSegIio m) (Monotone.functor ⋯ ⋙ F))
have hf : Monotone f
Tactic: have hf : Monotone f := fun _ _ h ↦ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
⊢ hf.functor.Final
have rw : ∀ (j₂ : (↑(Set.Iio (↑m : J)) : Type w)), ∃ (j₁ : (↑(Set.Iio m) : Type w)), j₂ ≤ f j₁
Tactic: rw [Monotone.final_functor_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj' : j' ∈ Set.Iio (↑m : J)
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)), Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj' ≤ f j₁
have hj'₁ : j' < (↑m : J)
Tactic: push _ ∈ _ at hj'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)), Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤ f j₁
have dsimp : ∃ (j₁ : (↑(Set.Iio m) : Type w)),
  Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) sorry
Tactic: dsimp only [f]