-- Mathlib/Order/Height.lean
theorem chainHeight_add_le_chainHeight_add (s : Set α) (t : Set β) (n m : ℕ) :
    s.chainHeight + n ≤ t.chainHeight + m ↔
      ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l + n ≤ length l' + m

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
⊢ ∃ l ∈ t.subchain, l.length = k

Tactic:
have := (le_chainHeight_TFAE t k).out 1 2

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
this : (∃ l ∈ t.subchain, l.length = k) ↔ ∃ l ∈ t.subchain, k ≤ l.length
⊢ ∃ l ∈ t.subchain, l.length = k

Proof state:
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ¬s.chainHeight = ⊤
k : ℕ
hk : ↑k = s.chainHeight
l : List α
hs : l ∈ s.subchain
hl : l.length = k
⊢ ↑l.length + ↑n ≤ t.chainHeight + ↑m

Tactic:
exact le_chainHeight_add_nat_iff.2 (H l hs)

Result:
no goals

Proof state:
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ¬s.chainHeight = ⊤
k : ℕ
hk : ↑k = s.chainHeight
l : List α
hs : l ∈ s.subchain
hl : l.length = k
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Tactic:
rw [← hk, ← hl]

Result:
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ¬s.chainHeight = ⊤
k : ℕ
hk : ↑k = s.chainHeight
l : List α
hs : l ∈ s.subchain
hl : l.length = k
⊢ ↑l.length + ↑n ≤ t.chainHeight + ↑m

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : s.chainHeight = ⊤
⊢ t.chainHeight = ⊤

Tactic:
rw [chainHeight_eq_top_iff] at h ⊢

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
⊢ ∀ (n : ℕ), ∃ l ∈ t.subchain, l.length = n

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : s.chainHeight = ⊤
this : t.chainHeight = ⊤
⊢ s.chainHeight + ↑n ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ¬s.chainHeight = ⊤
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Tactic:
obtain ⟨k, hk⟩ := WithTop.ne_top_iff_exists.1 h

Result:
case neg.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ¬s.chainHeight = ⊤
k : ℕ
hk : ↑k = s.chainHeight
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Proof state:
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
this : (∃ l ∈ t.subchain, l.length = k) ↔ ∃ l ∈ t.subchain, k ≤ l.length
l : List α
hs : l ∈ s.subchain
hl : l.length = k + m
l' : List β
ht : l' ∈ t.subchain
hl' : l.length + n ≤ l'.length + m
⊢ ∃ l ∈ t.subchain, k ≤ l.length

Tactic:
exact ⟨l', ht, (add_le_add_iff_right m).1 <| _root_.trans (hl.symm.trans_le le_self_add) hl'⟩

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
this : (∃ l ∈ t.subchain, l.length = k) ↔ ∃ l ∈ t.subchain, k ≤ l.length
l : List α
hs : l ∈ s.subchain
hl : l.length = k + m
⊢ ∃ l ∈ t.subchain, k ≤ l.length

Tactic:
obtain ⟨l', ht, hl'⟩ := H l hs

Result:
case pos.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
this : (∃ l ∈ t.subchain, l.length = k) ↔ ∃ l ∈ t.subchain, k ≤ l.length
l : List α
hs : l ∈ s.subchain
hl : l.length = k + m
l' : List β
ht : l' ∈ t.subchain
hl' : l.length + n ≤ l'.length + m
⊢ ∃ l ∈ t.subchain, k ≤ l.length

Proof state:
case neg.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ¬s.chainHeight = ⊤
k : ℕ
hk : ↑k = s.chainHeight
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Tactic:
obtain ⟨l, hs, hl⟩ := le_chainHeight_iff.1 hk.le

Result:
case neg.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ¬s.chainHeight = ⊤
k : ℕ
hk : ↑k = s.chainHeight
l : List α
hs : l ∈ s.subchain
hl : l.length = k
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
this : (∃ l ∈ t.subchain, l.length = k) ↔ ∃ l ∈ t.subchain, k ≤ l.length
⊢ ∃ l ∈ t.subchain, l.length = k

Tactic:
rw [this]

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
this : (∃ l ∈ t.subchain, l.length = k) ↔ ∃ l ∈ t.subchain, k ≤ l.length
⊢ ∃ l ∈ t.subchain, k ≤ l.length

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m

Tactic:
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 ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : s.chainHeight = ⊤
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Tactic:
suffices t.chainHeight = ⊤ by
  rw [this, top_add]
  exact le_top

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : s.chainHeight = ⊤
⊢ t.chainHeight = ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : s.chainHeight = ⊤
this : t.chainHeight = ⊤
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Tactic:
rw [this, top_add]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : s.chainHeight = ⊤
this : t.chainHeight = ⊤
⊢ s.chainHeight + ↑n ≤ ⊤