α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m ↔
    ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
refine'
  ⟨fun e l h ↦
    le_chainHeight_add_nat_iff.1
      ((add_le_add_right (length_le_chainHeight_of_mem_subchain h) _).trans e),
    fun H ↦ _⟩
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : chainHeight s = ⊤
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ¬chainHeight s = ⊤
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
by_cases s.chainHeight = ⊤
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : chainHeight s = ⊤
⊢ chainHeight t = ⊤
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : chainHeight s = ⊤
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
suffices t.chainHeight = ⊤ by
  rw [this, top_add]
  exact le_top
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
⊢ ∀ (n : ℕ), ∃ l, l ∈ subchain t ∧ length l = n
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : chainHeight s = ⊤
⊢ chainHeight t = ⊤
rw [chainHeight_eq_top_iff] at h⊢
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
⊢ ∃ l, l ∈ subchain t ∧ length l = k
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
⊢ ∀ (n : ℕ), ∃ l, l ∈ subchain t ∧ length l = n
intro k
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
this : (∃ l, l ∈ subchain t ∧ length l = k) ↔ ∃ l, l ∈ subchain t ∧ k ≤ length l
⊢ ∃ l, l ∈ subchain t ∧ length l = k
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
⊢ ∃ l, l ∈ subchain t ∧ length l = k
have := (le_chainHeight_TFAE t k).out 1 2
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
this : (∃ l, l ∈ subchain t ∧ length l = k) ↔ ∃ l, l ∈ subchain t ∧ k ≤ length l
⊢ ∃ l, l ∈ subchain t ∧ k ≤ length l
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
this : (∃ l, l ∈ subchain t ∧ length l = k) ↔ ∃ l, l ∈ subchain t ∧ k ≤ length l
⊢ ∃ l, l ∈ subchain t ∧ length l = k
rw [this]
case pos.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
this : (∃ l, l ∈ subchain t ∧ length l = k) ↔ ∃ l, l ∈ subchain t ∧ k ≤ length l
l : List α
hs : l ∈ subchain s
hl : length l = k + m
⊢ ∃ l, l ∈ subchain t ∧ k ≤ length l
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
this : (∃ l, l ∈ subchain t ∧ length l = k) ↔ ∃ l, l ∈ subchain t ∧ k ≤ length l
⊢ ∃ l, l ∈ subchain t ∧ k ≤ length l
obtain ⟨l, hs, hl⟩ := h (k + m)
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
this : (∃ l, l ∈ subchain t ∧ length l = k) ↔ ∃ l, l ∈ subchain t ∧ k ≤ length l
l : List α
hs : l ∈ subchain s
hl : length l = k + m
l' : List β
ht : l' ∈ subchain t
hl' : length l + n ≤ length l' + m
⊢ ∃ l, l ∈ subchain t ∧ k ≤ length l
case pos.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
this : (∃ l, l ∈ subchain t ∧ length l = k) ↔ ∃ l, l ∈ subchain t ∧ k ≤ length l
l : List α
hs : l ∈ subchain s
hl : length l = k + m
⊢ ∃ l, l ∈ subchain t ∧ k ≤ length l
obtain ⟨l', ht, hl'⟩ := H l hs
no goals
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
k : ℕ
this : (∃ l, l ∈ subchain t ∧ length l = k) ↔ ∃ l, l ∈ subchain t ∧ k ≤ length l
l : List α
hs : l ∈ subchain s
hl : length l = k + m
l' : List β
ht : l' ∈ subchain t
hl' : length l + n ≤ length l' + m
⊢ ∃ l, l ∈ subchain t ∧ k ≤ length l
exact ⟨l', ht, (add_le_add_iff_right m).1 <| _root_.trans (hl.symm.trans_le le_self_add) hl'⟩
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : chainHeight s = ⊤
this : chainHeight t = ⊤
⊢ chainHeight s + ↑n ≤ ⊤
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : chainHeight s = ⊤
this : chainHeight t = ⊤
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
rw [this, top_add]
no goals
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : chainHeight s = ⊤
this : chainHeight t = ⊤
⊢ chainHeight s + ↑n ≤ ⊤
exact le_top
case neg.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ¬chainHeight s = ⊤
k : ℕ
hk : ↑k = chainHeight s
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ¬chainHeight s = ⊤
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
obtain ⟨k, hk⟩ := WithTop.ne_top_iff_exists.1 h
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ¬chainHeight s = ⊤
k : ℕ
hk : ↑k = chainHeight s
l : List α
hs : l ∈ subchain s
hl : length l = k
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
case neg.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ¬chainHeight s = ⊤
k : ℕ
hk : ↑k = chainHeight s
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
obtain ⟨l, hs, hl⟩ := le_chainHeight_iff.1 hk.le
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ¬chainHeight s = ⊤
k : ℕ
hk : ↑k = chainHeight s
l : List α
hs : l ∈ subchain s
hl : length l = k
⊢ ↑(length l) + ↑n ≤ chainHeight t + ↑m
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ¬chainHeight s = ⊤
k : ℕ
hk : ↑k = chainHeight s
l : List α
hs : l ∈ subchain s
hl : length l = k
⊢ chainHeight s + ↑n ≤ chainHeight t + ↑m
rw [← hk, ← hl]
no goals
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
n m : ℕ
H : ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l + n ≤ length l' + m
h : ¬chainHeight s = ⊤
k : ℕ
hk : ↑k = chainHeight s
l : List α
hs : l ∈ subchain s
hl : length l = k
⊢ ↑(length l) + ↑n ≤ chainHeight t + ↑m
exact le_chainHeight_add_nat_iff.2 (H l hs)