case a
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)

case a
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
⊢ (⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)) ≤ chainHeight s
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s = ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
apply le_antisymm
case a
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
⊢ ∀ (i : List α), i ∈ subchain s → ↑(length i) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
case a
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
refine' iSup₂_le _
case a.nil
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
h : [] ∈ subchain s
⊢ ↑(length []) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)

case a.cons
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ ↑(length (x :: xs)) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
case a
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
⊢ ∀ (i : List α), i ∈ subchain s → ↑(length i) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
rintro (_ | ⟨x, xs⟩) h
no goals
case a.nil
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
h : [] ∈ subchain s
⊢ ↑(length []) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
exact zero_le _
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ ↑(length (x :: xs)) ≤ chainHeight (s ∩ Ici x)
case a.cons
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ ↑(length (x :: xs)) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
apply le_trans _ (le_iSup₂ x (cons_mem_subchain_iff.mp h).1)
case hl
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ x :: xs ∈ subchain (s ∩ Ici x)
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ ↑(length (x :: xs)) ≤ chainHeight (s ∩ Ici x)
apply length_le_chainHeight_of_mem_subchain
case hl
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
hi : i ∈ x :: xs
⊢ i ∈ Ici x
case hl
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ x :: xs ∈ subchain (s ∩ Ici x)
refine' ⟨h.1, fun i hi ↦ ⟨h.2 i hi, _⟩⟩
case hl.head
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ x ∈ Ici x

case hl.tail
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
a✝ : Mem i xs
⊢ i ∈ Ici x
case hl
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
hi : i ∈ x :: xs
⊢ i ∈ Ici x
cases hi
case hl.tail
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
hi : Mem i xs
⊢ i ∈ Ici x
case hl.tail
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
a✝ : Mem i xs
⊢ i ∈ Ici x
rename_i hi
case hl.tail.cons
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
hi : Mem i xs
a✝ : List.Pairwise (fun x x_1 => x < x_1) xs
h' : ∀ (a' : α), a' ∈ xs → x < a'
⊢ i ∈ Ici x
case hl.tail
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
hi : Mem i xs
⊢ i ∈ Ici x
cases' chain'_iff_pairwise.mp h.1 with _ _ h'
no goals
case hl.tail.cons
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
hi : Mem i xs
a✝ : List.Pairwise (fun x x_1 => x < x_1) xs
h' : ∀ (a' : α), a' ∈ xs → x < a'
⊢ i ∈ Ici x
exact (h' _ hi).le
no goals
case hl.head
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ x ∈ Ici x
exact left_mem_Ici
no goals
case a
α : Type u_1
β : Type ?u.32030
s t : Set α
inst✝ : Preorder α
⊢ (⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)) ≤ chainHeight s
exact iSup₂_le fun i _ ↦ chainHeight_mono <| Set.inter_subset_left _ _