-- Mathlib/CategoryTheory/Limits/Shapes/Preorder/HasIterationOfShape.lean
lemma hasColimitsOfShape_of_initialSeg
    {α : Type*} [LinearOrder α] (f : α ≤i J) [Nonempty α] :
    HasColimitsOfShape α C

Proof state:
case neg.intro
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
i : J
hi₀ : i = s.top
⊢ HasColimitsOfShape α C

Tactic:
induction i using SuccOrder.limitRecOn with
| hm i hi =>
  subst hi₀
  exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim
| hs 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
| hl i hi =>
  subst hi₀
  exact hasColimitsOfShape_of_isSuccLimit' C s hi

Result:
no goals

Proof state:
case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
⊢ HasColimitsOfShape α C

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

Result:
case neg.intro
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
i : J
hi₀ : i = s.top
⊢ HasColimitsOfShape α C

Proof state:
case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
⊢ HasColimitsOfShape α C

Tactic:
let s := f.toPrincipalSeg hf

Result:
case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
⊢ HasColimitsOfShape α C

Proof state:
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
i : J
hi : ¬IsMax i
a✝ : i = s.top → HasColimitsOfShape α C
hi₀ : Order.succ i = s.top
⊢ i < s.top

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

Result:
no goals

Proof state:
case neg.intro.hs.intro
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
⊢ HasColimitsOfShape α 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) }

Result:
case neg.intro.hs.intro
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
this : OrderTop α
⊢ HasColimitsOfShape α C

Proof state:
case neg.intro.hm
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
hi : IsMin s.top
⊢ HasColimitsOfShape α C

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

Result:
no goals

Proof state:
case neg.intro.hl
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : (fun x1 x2 => x1 < x2) ≺i fun x1 x2 => x1 < x2 := f.toPrincipalSeg hf
hi : Order.IsSuccLimit s.top
a✝ : ∀ b < s.top, b = s.top → HasColimitsOfShape α C
⊢ HasColimitsOfShape α C

Tactic:
exact hasColimitsOfShape_of_isSuccLimit' C s hi

Result:
no goals