-- Mathlib/Order/Height.lean
theorem chainHeight_eq_iSup_Ici : s.chainHeight = ⨆ i ∈ s, (s ∩ Set.Ici i).chainHeight

Proof state:
case hl.head
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
⊢ x ∈ Ici x

Tactic:
exact left_mem_Ici

Result:
no goals

Proof state:
case hl
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
i : α
hi : i ∈ x :: xs
⊢ i ∈ Ici x

Tactic:
cases hi

Result:
case hl.head
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
⊢ x ∈ Ici x

case hl.tail
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
i : α
a✝ : Mem i xs
⊢ i ∈ Ici x

Proof state:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
⊢ ↑(x :: xs).length ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight

Tactic:
apply le_trans _ (le_iSup₂ x (cons_mem_subchain_iff.mp h).1)

Result:
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
⊢ ↑(x :: xs).length ≤ (s ∩ Ici x).chainHeight

Proof state:
case hl.tail
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
i : α
hi : Mem i xs
⊢ i ∈ Ici x

Tactic:
obtain - | h' := chain'_iff_pairwise.mp h.1

Result:
case hl.tail.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
i : α
hi : Mem i xs
a✝ : List.Pairwise (fun x1 x2 => x1 < x2) xs
h' : ∀ a' ∈ xs, x < a'
⊢ i ∈ Ici x

Proof state:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ ∀ i ∈ s.subchain, ↑i.length ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight

Tactic:
rintro (_ | ⟨x, xs⟩) h

Result:
case a.nil
α : Type u_1
s : Set α
inst✝ : Preorder α
h : [] ∈ s.subchain
⊢ ↑[].length ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight

case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
⊢ ↑(x :: xs).length ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight

Proof state:
case hl.tail.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
i : α
hi : Mem i xs
a✝ : List.Pairwise (fun x1 x2 => x1 < x2) xs
h' : ∀ a' ∈ xs, x < a'
⊢ i ∈ Ici x

Tactic:
exact (h' _ hi).le

Result:
no goals

Proof state:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ ⨆ i ∈ s, (s ∩ Ici i).chainHeight ≤ s.chainHeight

Tactic:
exact iSup₂_le fun i _ ↦ chainHeight_mono Set.inter_subset_left

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
⊢ ↑(x :: xs).length ≤ (s ∩ Ici x).chainHeight

Tactic:
apply length_le_chainHeight_of_mem_subchain

Result:
case hl
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
⊢ x :: xs ∈ (s ∩ Ici x).subchain

Proof state:
case a.nil
α : Type u_1
s : Set α
inst✝ : Preorder α
h : [] ∈ s.subchain
⊢ ↑[].length ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case hl.tail
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
i : α
a✝ : Mem i xs
⊢ i ∈ Ici x

Tactic:
rename_i hi

Result:
case hl.tail
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
i : α
hi : Mem i xs
⊢ i ∈ Ici x

Proof state:
case hl
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
⊢ x :: xs ∈ (s ∩ Ici x).subchain

Tactic:
refine ⟨h.1, fun i hi ↦ ⟨h.2 i hi, ?_⟩⟩

Result:
case hl
α : Type u_1
s : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ s.subchain
i : α
hi : i ∈ x :: xs
⊢ i ∈ Ici x

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ s.chainHeight = ⨆ i ∈ s, (s ∩ Ici i).chainHeight

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ s.chainHeight ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight

case a
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ ⨆ i ∈ s, (s ∩ Ici i).chainHeight ≤ s.chainHeight

Proof state:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ s.chainHeight ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight

Tactic:
refine iSup₂_le ?_

Result:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ ∀ i ∈ s.subchain, ↑i.length ≤ ⨆ i ∈ s, (s ∩ Ici i).chainHeight