-- Mathlib/CategoryTheory/Limits/Shapes/Preorder/HasIterationOfShape.lean
lemma hasColimitsOfShape_of_initialSeg
    {α : Type*} [LinearOrder α] (f : α ≤i J) [Nonempty α] :
    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
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ s.toRelEmbedding b < Order.succ (s.toRelEmbedding ⊤)

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

Result:
no goals

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 α
⊢ HasColimitsOfShape α C

Tactic:
by_cases hf : Function.Surjective f

Result:
case pos
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

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

Proof state:
case neg.intro.hs
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
⊢ HasColimitsOfShape α 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)

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
⊢ 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
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ b ≤ ⊤

Tactic:
rw [← s.le_iff_le]

Result:
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
b : α
⊢ s.toRelEmbedding b ≤ s.toRelEmbedding ⊤

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
this : OrderTop α
⊢ HasColimitsOfShape α C

Tactic:
infer_instance

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
i : J
hi : Order.IsSuccLimit i
a✝ : ∀ b < i, b = s.top → HasColimitsOfShape α C
hi₀ : i = s.top
⊢ HasColimitsOfShape α C

Tactic:
subst hi₀

Result:
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

Proof state:
case pos
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:
exact hasColimitsOfShape_of_equivalence
  (OrderIso.ofRelIsoLT (RelIso.ofSurjective f.toRelEmbedding hf)).equivalence.symm

Result:
no goals

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
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ s.toRelEmbedding b ≤ s.toRelEmbedding ⊤

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

Result:
no goals

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
i : J
hi : IsMin i
hi₀ : i = s.top
⊢ HasColimitsOfShape α C

Tactic:
subst hi₀

Result:
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