-- Mathlib/Order/Height.lean
theorem chainHeight_union_eq (s t : Set α) (H : ∀ a ∈ s, ∀ b ∈ t, a < b) :
    (s ∪ t).chainHeight = s.chainHeight + t.chainHeight

Proof state:
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
⊢ l.length + l'.length ≤ (l ++ l').length + 0

Tactic:
simp

Result:
no goals

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
h : t.chainHeight = ⊤
⊢ t.chainHeight ≤ (s ∪ t).chainHeight

Tactic:
exact Set.chainHeight_mono subset_union_right

Result:
no goals

Proof state:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ (s ∪ t).chainHeight ≤ s.chainHeight + t.chainHeight

Tactic:
exact chainHeight_union_le

Result:
no goals

Proof state:
case coe.a.intro.intro.refine_1
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
x : α
hx : x ∈ l.getLast?
y : α
hy : y ∈ l'.head?
⊢ x < y

Tactic:
exact H x (hl.2 _ <| mem_of_mem_getLast? hx) y (hl'.2 _ <| mem_of_mem_head? hy)

Result:
no goals

Proof state:
case coe.a.intro.intro.refine_2
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
i : α
hi : i ∈ l ∨ i ∈ l'
⊢ i ∈ s ∪ t

Tactic:
rcases hi with hi | hi

Result:
case coe.a.intro.intro.refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
i : α
hi : i ∈ l
⊢ i ∈ s ∪ t

case coe.a.intro.intro.refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
i : α
hi : i ∈ l'
⊢ i ∈ s ∪ t

Proof state:
case coe.a.intro.intro.refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
i : α
hi : i ∈ l
⊢ i ∈ s ∪ t

case coe.a.intro.intro.refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
i : α
hi : i ∈ l'
⊢ i ∈ s ∪ t

Tactic:
exacts [Or.inl (hl.2 _ hi), Or.inr (hl'.2 _ hi)]

Result:
no goals

Proof state:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ (s ∪ t).chainHeight ≤ s.chainHeight + ↑a✝

Tactic:
rw [← h]

Result:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ (s ∪ t).chainHeight ≤ s.chainHeight + t.chainHeight

Proof state:
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
⊢ (s ∪ t).chainHeight = s.chainHeight + t.chainHeight

Tactic:
cases h : t.chainHeight

Result:
case top
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
h : t.chainHeight = ⊤
⊢ (s ∪ t).chainHeight = s.chainHeight + ⊤

case coe
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ (s ∪ t).chainHeight = s.chainHeight + ↑a✝

Proof state:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ ∀ l ∈ s.subchain, ∃ l' ∈ (s ∪ t).subchain, l.length + a✝ ≤ l'.length + 0

Tactic:
intro l hl

Result:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
l : List α
hl : l ∈ s.subchain
⊢ ∃ l' ∈ (s ∪ t).subchain, l.length + a✝ ≤ l'.length + 0

Proof state:
case coe
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ (s ∪ t).chainHeight = s.chainHeight + ↑a✝

Tactic:
apply le_antisymm

Result:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ (s ∪ t).chainHeight ≤ s.chainHeight + ↑a✝

case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ s.chainHeight + ↑a✝ ≤ (s ∪ t).chainHeight

Proof state:
case coe.a.intro.intro.refine_2
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
i : α
hi : i ∈ l ++ l'
⊢ i ∈ s ∪ t

Tactic:
rw [mem_append] at hi

Result:
case coe.a.intro.intro.refine_2
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
i : α
hi : i ∈ l ∨ i ∈ l'
⊢ i ∈ s ∪ t

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
h : t.chainHeight = ⊤
⊢ (s ∪ t).chainHeight = s.chainHeight + ⊤

Tactic:
rw [add_top, eq_top_iff, ← h]

Result:
case top
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
h : t.chainHeight = ⊤
⊢ t.chainHeight ≤ (s ∪ t).chainHeight

Proof state:
case coe.a.intro.intro
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
⊢ ∃ l'_1 ∈ (s ∪ t).subchain, l.length + l'.length ≤ l'_1.length + 0

Tactic:
refine ⟨l ++ l', ⟨Chain'.append hl.1 hl'.1 fun x hx y hy ↦ ?_, fun i hi ↦ ?_⟩, by simp⟩

Result:
case coe.a.intro.intro.refine_1
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
x : α
hx : x ∈ l.getLast?
y : α
hy : y ∈ l'.head?
⊢ x < y

case coe.a.intro.intro.refine_2
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
i : α
hi : i ∈ l ++ l'
⊢ i ∈ s ∪ t

Proof state:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ s.chainHeight + ↑a✝ ≤ (s ∪ t).chainHeight

Tactic:
rw [← add_zero (s ∪ t).chainHeight, ← WithTop.coe_zero,
  ENat.some_eq_coe, chainHeight_add_le_chainHeight_add]

Result:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
⊢ ∀ l ∈ s.subchain, ∃ l' ∈ (s ∪ t).subchain, l.length + a✝ ≤ l'.length + 0

Proof state:
case coe.a
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
a✝ : ℕ
h : t.chainHeight = ↑a✝
l : List α
hl : l ∈ s.subchain
⊢ ∃ l' ∈ (s ∪ t).subchain, l.length + a✝ ≤ l'.length + 0

Tactic:
obtain ⟨l', hl', rfl⟩ := exists_chain_of_le_chainHeight t h.symm.le

Result:
case coe.a.intro.intro
α : Type u_1
inst✝ : Preorder α
s t : Set α
H : ∀ a ∈ s, ∀ b ∈ t, a < b
l : List α
hl : l ∈ s.subchain
l' : List α
hl' : l' ∈ t.subchain
h : t.chainHeight = ↑l'.length
⊢ ∃ l'_1 ∈ (s ∪ t).subchain, l.length + l'.length ≤ l'_1.length + 0