case none
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
h : chainHeight t = none
⊢ chainHeight (s ∪ t) = chainHeight s + none

case some
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ chainHeight (s ∪ t) = chainHeight s + some val✝
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
⊢ chainHeight (s ∪ t) = chainHeight s + chainHeight t
cases h : t.chainHeight
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ chainHeight (s ∪ t) ≤ chainHeight s + some val✝

case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ chainHeight s + some val✝ ≤ chainHeight (s ∪ t)
case some
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ chainHeight (s ∪ t) = chainHeight s + some val✝
apply le_antisymm
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (s ∪ t) ∧ length l + val✝ ≤ length l' + 0
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ chainHeight s + some val✝ ≤ chainHeight (s ∪ t)
rw [WithTop.some_eq_coe, ← add_zero (s ∪ t).chainHeight, ← WithTop.coe_zero,
  ENat.some_eq_coe, chainHeight_add_le_chainHeight_add]
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
l : List α
hl : l ∈ subchain s
⊢ ∃ l', l' ∈ subchain (s ∪ t) ∧ length l + val✝ ≤ length l' + 0
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (s ∪ t) ∧ length l + val✝ ≤ length l' + 0
intro l hl
case some.a.intro.intro
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
⊢ ∃ l'_1, l'_1 ∈ subchain (s ∪ t) ∧ length l + length l' ≤ length l'_1 + 0
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
l : List α
hl : l ∈ subchain s
⊢ ∃ l', l' ∈ subchain (s ∪ t) ∧ length l + val✝ ≤ length l' + 0
obtain ⟨l', hl', rfl⟩ := exists_chain_of_le_chainHeight t h.symm.le
case some.a.intro.intro.refine'_1
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
x : α
hx : x ∈ getLast? l
y : α
hy : y ∈ head? l'
⊢ x < y

case some.a.intro.intro.refine'_2
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
i : α
hi : i ∈ l ++ l'
⊢ i ∈ s ∪ t
case some.a.intro.intro
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
⊢ ∃ l'_1, l'_1 ∈ subchain (s ∪ t) ∧ length l + length l' ≤ length l'_1 + 0
refine' ⟨l ++ l', ⟨Chain'.append hl.1 hl'.1 fun x hx y hy ↦ _, fun i hi ↦ _⟩, by simp⟩
case none
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
h : chainHeight t = none
⊢ chainHeight t ≤ chainHeight (s ∪ t)
case none
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
h : chainHeight t = none
⊢ chainHeight (s ∪ t) = chainHeight s + none
rw [WithTop.none_eq_top, add_top, eq_top_iff, ← WithTop.none_eq_top, ← h]
no goals
case none
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
h : chainHeight t = none
⊢ chainHeight t ≤ chainHeight (s ∪ t)
exact Set.chainHeight_mono (Set.subset_union_right _ _)
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ chainHeight (s ∪ t) ≤ chainHeight s + chainHeight t
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ chainHeight (s ∪ t) ≤ chainHeight s + some val✝
rw [← h]
no goals
case some.a
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
val✝ : ℕ
h : chainHeight t = some val✝
⊢ chainHeight (s ∪ t) ≤ chainHeight s + chainHeight t
exact chainHeight_union_le
no goals
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
⊢ length l + length l' ≤ length (l ++ l') + 0
simp
no goals
case some.a.intro.intro.refine'_1
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
x : α
hx : x ∈ getLast? l
y : α
hy : y ∈ head? l'
⊢ x < y
exact H x (hl.2 _ <| mem_of_mem_getLast? hx) y (hl'.2 _ <| mem_of_mem_head? hy)
case some.a.intro.intro.refine'_2
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
i : α
hi : i ∈ l ∨ i ∈ l'
⊢ i ∈ s ∪ t
case some.a.intro.intro.refine'_2
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
i : α
hi : i ∈ l ++ l'
⊢ i ∈ s ∪ t
rw [mem_append] at hi
case some.a.intro.intro.refine'_2.inl
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
i : α
hi : i ∈ l
⊢ i ∈ s ∪ t

case some.a.intro.intro.refine'_2.inr
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
i : α
hi : i ∈ l'
⊢ i ∈ s ∪ t
case some.a.intro.intro.refine'_2
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
i : α
hi : i ∈ l ∨ i ∈ l'
⊢ i ∈ s ∪ t
cases' hi with hi hi
no goals
case some.a.intro.intro.refine'_2.inl
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
i : α
hi : i ∈ l
⊢ i ∈ s ∪ t

case some.a.intro.intro.refine'_2.inr
α : Type u_1
β : Type ?u.43133
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
l : List α
hl : l ∈ subchain s
l' : List α
hl' : l' ∈ subchain t
h : chainHeight t = some (length l')
i : α
hi : i ∈ l'
⊢ i ∈ s ∪ t
exacts [Or.inl (hl.2 _ hi), Or.inr (hl'.2 _ hi)]