[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ a :: l ∈ subchain s ↔ a ∈ s ∧ l ∈ subchain s ∧ ∀ (b : α), b ∈ head? l → a < b
[PROOFSTEP]
simp only [subchain, mem_setOf_eq, forall_mem_cons, chain'_cons', and_left_comm, and_comm, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ [a] ∈ subchain s ↔ a ∈ s
[PROOFSTEP]
simp [cons_mem_subchain_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
⊢ ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
cases' (le_top : s.chainHeight ≤ ⊤).eq_or_lt with ha ha
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : chainHeight s = ⊤
⊢ ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
rw [chainHeight_eq_iSup_subtype] at ha 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : chainHeight s < ⊤
⊢ ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
rw [chainHeight_eq_iSup_subtype] at ha 
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : ⨆ (l : ↑(subchain s)), ↑(length ↑l) = ⊤
⊢ ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
obtain ⟨_, ⟨⟨l, h₁, h₂⟩, rfl⟩, h₃⟩ := not_bddAbove_iff'.mp ((WithTop.iSup_coe_eq_top _).mp ha) n
[GOAL]
case inl.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : ⨆ (l : ↑(subchain s)), ↑(length ↑l) = ⊤
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
h₃ :
  ¬(fun x => ↑(length ↑x)) { val := l, property := (_ : Chain' (fun x x_1 => x < x_1) l ∧ ∀ (i : α), i ∈ l → i ∈ s) } ≤
      n
⊢ ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
exact
  ⟨l.take n, ⟨h₁.take _, fun x h ↦ h₂ _ <| take_subset _ _ h⟩,
    (l.length_take n).trans <| min_eq_left <| le_of_not_ge h₃⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : ⨆ (l : ↑(subchain s)), ↑(length ↑l) < ⊤
⊢ ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
rw [ENat.iSup_coe_lt_top] at ha 
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
⊢ ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
obtain ⟨⟨l, h₁, h₂⟩, e : l.length = _⟩ := Nat.sSup_mem (Set.range_nonempty _) ha
[GOAL]
case inr.intro.mk.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
e : length l = sSup (range fun l => length ↑l)
⊢ ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
refine' ⟨l.take n, ⟨h₁.take _, fun x h ↦ h₂ _ <| take_subset _ _ h⟩, (l.length_take n).trans <| min_eq_left <| _⟩
[GOAL]
case inr.intro.mk.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
hn : ↑n ≤ chainHeight s
ha : BddAbove (range fun l => length ↑l)
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
e : length l = sSup (range fun l => length ↑l)
⊢ n ≤ length l
[PROOFSTEP]
rwa [e, ← Nat.cast_le (α := ℕ∞), sSup_range, ENat.coe_iSup ha, ← chainHeight_eq_iSup_subtype]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
⊢ ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
exact s.exists_chain_of_le_chainHeight
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
⊢ (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
[PROOFSTEP]
rintro ⟨l, hls, he⟩
[GOAL]
case tfae_2_to_3.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
l : List α
hls : l ∈ subchain s
he : length l = n
⊢ ∃ l, l ∈ subchain s ∧ n ≤ length l
[PROOFSTEP]
exact ⟨l, hls, he.ge⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
[PROOFSTEP]
tfae_have 3 → 1
[GOAL]
case tfae_3_to_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
⊢ (∃ l, l ∈ subchain s ∧ n ≤ length l) → ↑n ≤ chainHeight s
[PROOFSTEP]
rintro ⟨l, hs, hn⟩
[GOAL]
case tfae_3_to_1.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
l : List α
hs : l ∈ subchain s
hn : n ≤ length l
⊢ ↑n ≤ chainHeight s
[PROOFSTEP]
exact le_iSup₂_of_le l hs (WithTop.coe_le_coe.2 hn)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n : ℕ
tfae_1_to_2 : ↑n ≤ chainHeight s → ∃ l, l ∈ subchain s ∧ length l = n
tfae_2_to_3 : (∃ l, l ∈ subchain s ∧ length l = n) → ∃ l, l ∈ subchain s ∧ n ≤ length l
tfae_3_to_1 : (∃ l, l ∈ subchain s ∧ n ≤ length l) → ↑n ≤ chainHeight s
⊢ TFAE [↑n ≤ chainHeight s, ∃ l, l ∈ subchain s ∧ length l = n, ∃ l, l ∈ subchain s ∧ n ≤ length l]
[PROOFSTEP]
tfae_finish
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ chainHeight s = ⊤ ↔ ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
[PROOFSTEP]
refine' ⟨fun h n ↦ le_chainHeight_iff.1 (le_top.trans_eq h.symm), fun h ↦ _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : ∀ (n : ℕ), ∃ l, l ∈ subchain s ∧ length l = n
⊢ chainHeight s = ⊤
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : chainHeight s ≠ ⊤
⊢ ∃ n, ∀ (l : List α), l ∈ subchain s → length l ≠ n
[PROOFSTEP]
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 h
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
h : chainHeight s ≠ ⊤
n : ℕ
hn : ↑n = chainHeight s
⊢ ∃ n, ∀ (l : List α), l ∈ subchain s → length l ≠ n
[PROOFSTEP]
exact
  ⟨n + 1, fun l hs ↦
    (Nat.lt_succ_iff.2 <| Nat.cast_le.1 <| (length_le_chainHeight_of_mem_subchain hs).trans_eq hn.symm).ne⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ 1 ≤ chainHeight s ↔ Set.Nonempty s
[PROOFSTEP]
rw [← Nat.cast_one, Set.le_chainHeight_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ (∃ l, l ∈ subchain s ∧ length l = 1) ↔ Set.Nonempty s
[PROOFSTEP]
simp only [length_eq_one, @and_comm (_ ∈ _), @eq_comm _ _ [_], exists_exists_eq_and, singleton_mem_subchain_iff,
  Set.Nonempty]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ chainHeight s = 0 ↔ s = ∅
[PROOFSTEP]
rw [← not_iff_not, ← Ne.def, ← ENat.one_le_iff_ne_zero, one_le_chainHeight_iff, nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
n m : ℕ
⊢ ↑n ≤ chainHeight s + ↑m ↔ ∃ l, l ∈ subchain s ∧ n ≤ length l + m
[PROOFSTEP]
simp_rw [← tsub_le_iff_right, ← ENat.coe_sub, (le_chainHeight_TFAE s (n - m)).out 0 2]
[GOAL]
α : 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
[PROOFSTEP]
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 ↦ _⟩
[GOAL]
α : 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
[PROOFSTEP]
by_cases s.chainHeight = ⊤
[GOAL]
α : 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
[PROOFSTEP]
by_cases s.chainHeight = ⊤
[GOAL]
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
[PROOFSTEP]
suffices t.chainHeight = ⊤ by
  rw [this, top_add]
  exact le_top
[GOAL]
α : 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
[PROOFSTEP]
rw [this, top_add]
[GOAL]
α : 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 ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
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 = ⊤
[PROOFSTEP]
rw [chainHeight_eq_top_iff] at h ⊢
[GOAL]
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
[PROOFSTEP]
intro k
[GOAL]
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
[PROOFSTEP]
have := (le_chainHeight_TFAE t k).out 1 2
[GOAL]
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
[PROOFSTEP]
rw [this]
[GOAL]
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
[PROOFSTEP]
obtain ⟨l, hs, hl⟩ := h (k + m)
[GOAL]
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
[PROOFSTEP]
obtain ⟨l', ht, hl'⟩ := H l hs
[GOAL]
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
[PROOFSTEP]
exact ⟨l', ht, (add_le_add_iff_right m).1 <| _root_.trans (hl.symm.trans_le le_self_add) hl'⟩
[GOAL]
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
[PROOFSTEP]
obtain ⟨k, hk⟩ := WithTop.ne_top_iff_exists.1 h
[GOAL]
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
[PROOFSTEP]
obtain ⟨l, hs, hl⟩ := le_chainHeight_iff.1 hk.le
[GOAL]
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
[PROOFSTEP]
rw [← hk, ← hl]
[GOAL]
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
[PROOFSTEP]
exact le_chainHeight_add_nat_iff.2 (H l hs)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
⊢ TFAE
    [chainHeight s ≤ chainHeight t, ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l',
      ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l']
[PROOFSTEP]
tfae_have 1 ↔ 3
[GOAL]
case tfae_1_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
⊢ chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
[PROOFSTEP]
convert ← chainHeight_add_le_chainHeight_add s t 0 0
[GOAL]
case h.e'_1.h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
⊢ chainHeight s + ↑0 = chainHeight s
[PROOFSTEP]
apply add_zero
[GOAL]
case h.e'_1.h.e'_4
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
⊢ chainHeight t + ↑0 = chainHeight t
[PROOFSTEP]
apply add_zero
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ TFAE
    [chainHeight s ≤ chainHeight t, ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l',
      ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l']
[PROOFSTEP]
tfae_have 2 ↔ 3
[GOAL]
case tfae_2_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ (∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l') ↔
    ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
[PROOFSTEP]
refine' forall₂_congr fun l hl ↦ _
[GOAL]
case tfae_2_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
l : List α
hl : l ∈ subchain s
⊢ (∃ l', l' ∈ subchain t ∧ length l = length l') ↔ ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
[PROOFSTEP]
simp_rw [← (le_chainHeight_TFAE t l.length).out 1 2, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
tfae_2_iff_3 :
  (∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l') ↔
    ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ TFAE
    [chainHeight s ≤ chainHeight t, ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l',
      ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l']
[PROOFSTEP]
tfae_finish
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ chainHeight (f '' s) = chainHeight s
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ chainHeight (f '' s) ≤ chainHeight s
[PROOFSTEP]
rw [chainHeight_le_chainHeight_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ chainHeight s ≤ chainHeight (f '' s)
[PROOFSTEP]
rw [chainHeight_le_chainHeight_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ length l = length l'
[PROOFSTEP]
suffices ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, map f l' = l
  by
  intro l hl
  obtain ⟨l', h₁, rfl⟩ := this l hl
  exact ⟨l', h₁, length_map _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
⊢ ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ length l = length l'
[PROOFSTEP]
intro l hl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
l : List β
hl : l ∈ subchain (f '' s)
⊢ ∃ l', l' ∈ subchain s ∧ length l = length l'
[PROOFSTEP]
obtain ⟨l', h₁, rfl⟩ := this l hl
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
this : ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
l' : List α
h₁ : l' ∈ subchain s
hl : map f l' ∈ subchain (f '' s)
⊢ ∃ l'_1, l'_1 ∈ subchain s ∧ length (map f l') = length l'_1
[PROOFSTEP]
exact ⟨l', h₁, length_map _ _⟩
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ (l : List β), l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
[PROOFSTEP]
intro l
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List β
⊢ l ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = l
[PROOFSTEP]
induction' l with x xs hx
[GOAL]
case a.nil
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ [] ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = []
[PROOFSTEP]
exact fun _ ↦ ⟨nil, ⟨trivial, fun x h ↦ (not_mem_nil x h).elim⟩, rfl⟩
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
⊢ x :: xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
[PROOFSTEP]
intro h
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
h : x :: xs ∈ subchain (f '' s)
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
[PROOFSTEP]
rw [cons_mem_subchain_iff] at h 
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : β
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
h : x ∈ f '' s ∧ xs ∈ subchain (f '' s) ∧ ∀ (b : β), b ∈ head? xs → x < b
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = x :: xs
[PROOFSTEP]
obtain ⟨⟨x, hx', rfl⟩, h₁, h₂⟩ := h
[GOAL]
case a.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
xs : List β
hx : xs ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = xs
x : α
hx' : x ∈ s
h₁ : xs ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? xs → f x < b
⊢ ∃ l', l' ∈ subchain s ∧ map f l' = f x :: xs
[PROOFSTEP]
obtain ⟨l', h₃, rfl⟩ := hx h₁
[GOAL]
case a.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
l' : List α
h₃ : l' ∈ subchain s
hx : map f l' ∈ subchain (f '' s) → ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = map f l'
h₁ : map f l' ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f l') → f x < b
⊢ ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = f x :: map f l'
[PROOFSTEP]
refine' ⟨x :: l', Set.cons_mem_subchain_iff.mpr ⟨hx', h₃, _⟩, rfl⟩
[GOAL]
case a.cons.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
l' : List α
h₃ : l' ∈ subchain s
hx : map f l' ∈ subchain (f '' s) → ∃ l'_1, l'_1 ∈ subchain s ∧ map f l'_1 = map f l'
h₁ : map f l' ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f l') → f x < b
⊢ ∀ (b : α), b ∈ head? l' → x < b
[PROOFSTEP]
cases l'
[GOAL]
case a.cons.intro.intro.intro.intro.intro.intro.nil
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
h₃ : [] ∈ subchain s
hx : map f [] ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = map f []
h₁ : map f [] ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f []) → f x < b
⊢ ∀ (b : α), b ∈ head? [] → x < b
[PROOFSTEP]
simp
[GOAL]
case a.cons.intro.intro.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
x : α
hx' : x ∈ s
head✝ : α
tail✝ : List α
h₃ : head✝ :: tail✝ ∈ subchain s
hx : map f (head✝ :: tail✝) ∈ subchain (f '' s) → ∃ l', l' ∈ subchain s ∧ map f l' = map f (head✝ :: tail✝)
h₁ : map f (head✝ :: tail✝) ∈ subchain (f '' s)
h₂ : ∀ (b : β), b ∈ head? (map f (head✝ :: tail✝)) → f x < b
⊢ ∀ (b : α), b ∈ head? (head✝ :: tail✝) → x < b
[PROOFSTEP]
simpa [← hf] using h₂
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (f '' s) ∧ length l = length l'
[PROOFSTEP]
intro l hl
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ ∃ l', l' ∈ subchain (f '' s) ∧ length l = length l'
[PROOFSTEP]
refine' ⟨l.map f, ⟨_, _⟩, _⟩
[GOAL]
case a.refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ Chain' (fun x x_1 => x < x_1) (map f l)
[PROOFSTEP]
simp_rw [chain'_map, ← hf]
[GOAL]
case a.refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ Chain' (fun a b => a < b) l
[PROOFSTEP]
exact hl.1
[GOAL]
case a.refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ ∀ (i : β), i ∈ map f l → i ∈ f '' s
[PROOFSTEP]
intro _ e
[GOAL]
case a.refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
i✝ : β
e : i✝ ∈ map f l
⊢ i✝ ∈ f '' s
[PROOFSTEP]
obtain ⟨a, ha, rfl⟩ := mem_map.mp e
[GOAL]
case a.refine'_2.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a✝ : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
a : α
ha : a ∈ l
e : f a ∈ map f l
⊢ f a ∈ f '' s
[PROOFSTEP]
exact Set.mem_image_of_mem _ (hl.2 _ ha)
[GOAL]
case a.refine'_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t : Set α
l✝ : List α
a : α
f : α → β
hf : ∀ {x y : α}, x < y ↔ f x < f y
s : Set α
l : List α
hl : l ∈ subchain s
⊢ length l = length (map f l)
[PROOFSTEP]
rw [length_map]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ chainHeight (↑ofDual ⁻¹' s) = chainHeight s
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ chainHeight (↑ofDual ⁻¹' s) ≤ chainHeight s
[PROOFSTEP]
rw [chainHeight_le_chainHeight_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ ∀ (l : List αᵒᵈ), l ∈ subchain (↑ofDual ⁻¹' s) → ∃ l', l' ∈ subchain s ∧ length l = length l'
[PROOFSTEP]
rintro l ⟨h₁, h₂⟩
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
l : List αᵒᵈ
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : αᵒᵈ), i ∈ l → i ∈ ↑ofDual ⁻¹' s
⊢ ∃ l', l' ∈ subchain s ∧ length l = length l'
[PROOFSTEP]
exact ⟨l.reverse, ⟨chain'_reverse.mpr h₁, fun i h ↦ h₂ i (mem_reverse.mp h)⟩, (length_reverse _).symm⟩
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ chainHeight s ≤ chainHeight (↑ofDual ⁻¹' s)
[PROOFSTEP]
rw [chainHeight_le_chainHeight_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (↑ofDual ⁻¹' s) ∧ length l = length l'
[PROOFSTEP]
rintro l ⟨h₁, h₂⟩
[GOAL]
case a.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l✝ : List α
a : α
l : List α
h₁ : Chain' (fun x x_1 => x < x_1) l
h₂ : ∀ (i : α), i ∈ l → i ∈ s
⊢ ∃ l', l' ∈ subchain (↑ofDual ⁻¹' s) ∧ length l = length l'
[PROOFSTEP]
exact ⟨l.reverse, ⟨chain'_reverse.mpr h₁, fun i h ↦ h₂ i (mem_reverse.mp h)⟩, (length_reverse _).symm⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s = ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
[PROOFSTEP]
refine' iSup₂_le _
[GOAL]
case a
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ ∀ (i : List α), i ∈ subchain s → ↑(length i) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
[PROOFSTEP]
rintro (_ | ⟨x, xs⟩) h
[GOAL]
case a.nil
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
h : [] ∈ subchain s
⊢ ↑(length []) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
[PROOFSTEP]
exact zero_le _
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ ↑(length (x :: xs)) ≤ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i)
[PROOFSTEP]
apply le_trans _ (le_iSup₂ x (cons_mem_subchain_iff.mp h).1)
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ ↑(length (x :: xs)) ≤ chainHeight (s ∩ Ici x)
[PROOFSTEP]
apply length_le_chainHeight_of_mem_subchain
[GOAL]
case hl
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ x :: xs ∈ subchain (s ∩ Ici x)
[PROOFSTEP]
refine' ⟨h.1, fun i hi ↦ ⟨h.2 i hi, _⟩⟩
[GOAL]
case hl
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
hi : i ∈ x :: xs
⊢ i ∈ Ici x
[PROOFSTEP]
cases hi
[GOAL]
case hl.head
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
⊢ x ∈ Ici x
[PROOFSTEP]
exact left_mem_Ici
[GOAL]
case hl.tail
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
a✝ : Mem i xs
⊢ i ∈ Ici x
[PROOFSTEP]
rename_i hi
[GOAL]
case hl.tail
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
x : α
xs : List α
h : x :: xs ∈ subchain s
i : α
hi : Mem i xs
⊢ i ∈ Ici x
[PROOFSTEP]
cases' chain'_iff_pairwise.mp h.1 with _ _ h'
[GOAL]
case hl.tail.cons
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact (h' _ hi).le
[GOAL]
case a
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Ici i) ≤ chainHeight s
[PROOFSTEP]
exact iSup₂_le fun i _ ↦ chainHeight_mono <| Set.inter_subset_left _ _
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s = ⨆ (i : α) (_ : i ∈ s), chainHeight (s ∩ Iic i)
[PROOFSTEP]
simp_rw [← chainHeight_dual (_ ∩ _)]
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ chainHeight s = ⨆ (i : α) (_ : i ∈ s), chainHeight (↑ofDual ⁻¹' (s ∩ Iic i))
[PROOFSTEP]
rw [← chainHeight_dual, chainHeight_eq_iSup_Ici]
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ ⨆ (i : αᵒᵈ) (_ : i ∈ ↑ofDual ⁻¹' s), chainHeight (↑ofDual ⁻¹' s ∩ Ici i) =
    ⨆ (i : α) (_ : i ∈ s), chainHeight (↑ofDual ⁻¹' (s ∩ Iic i))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) = chainHeight s + 1
[PROOFSTEP]
rw [← add_zero (insert a s).chainHeight]
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) + 0 = chainHeight s + 1
[PROOFSTEP]
change (insert a s).chainHeight + (0 : ℕ) = s.chainHeight + (1 : ℕ)
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) + ↑0 = chainHeight s + ↑1
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) + ↑0 ≤ chainHeight s + ↑1
[PROOFSTEP]
rw [chainHeight_add_le_chainHeight_add]
[GOAL]
case a
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight s + ↑1 ≤ chainHeight (insert a s) + ↑0
[PROOFSTEP]
rw [chainHeight_add_le_chainHeight_add]
[GOAL]
case a
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ ∀ (l : List α), l ∈ subchain (insert a s) → ∃ l', l' ∈ subchain s ∧ length l + 0 ≤ length l' + 1
[PROOFSTEP]
rintro (_ | ⟨y, ys⟩) h
[GOAL]
case a.nil
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
h : [] ∈ subchain (insert a s)
⊢ ∃ l', l' ∈ subchain s ∧ length [] + 0 ≤ length l' + 1
[PROOFSTEP]
exact ⟨[], nil_mem_subchain _, zero_le _⟩
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
y : α
ys : List α
h : y :: ys ∈ subchain (insert a s)
⊢ ∃ l', l' ∈ subchain s ∧ length (y :: ys) + 0 ≤ length l' + 1
[PROOFSTEP]
have h' := cons_mem_subchain_iff.mp h
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
y : α
ys : List α
h : y :: ys ∈ subchain (insert a s)
h' : y ∈ insert a s ∧ ys ∈ subchain (insert a s) ∧ ∀ (b : α), b ∈ head? ys → y < b
⊢ ∃ l', l' ∈ subchain s ∧ length (y :: ys) + 0 ≤ length l' + 1
[PROOFSTEP]
refine' ⟨ys, ⟨h'.2.1.1, fun i hi ↦ _⟩, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
y : α
ys : List α
h : y :: ys ∈ subchain (insert a s)
h' : y ∈ insert a s ∧ ys ∈ subchain (insert a s) ∧ ∀ (b : α), b ∈ head? ys → y < b
⊢ length (y :: ys) + 0 ≤ length ys + 1
[PROOFSTEP]
simp
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
y : α
ys : List α
h : y :: ys ∈ subchain (insert a s)
h' : y ∈ insert a s ∧ ys ∈ subchain (insert a s) ∧ ∀ (b : α), b ∈ head? ys → y < b
i : α
hi : i ∈ ys
⊢ i ∈ s
[PROOFSTEP]
apply (h'.2.1.2 i hi).resolve_left
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
y : α
ys : List α
h : y :: ys ∈ subchain (insert a s)
h' : y ∈ insert a s ∧ ys ∈ subchain (insert a s) ∧ ∀ (b : α), b ∈ head? ys → y < b
i : α
hi : i ∈ ys
⊢ ¬i = a
[PROOFSTEP]
rintro rfl
[GOAL]
case a.cons
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ (b : α), b ∈ s → i < b
h : y :: ys ∈ subchain (insert i s)
h' : y ∈ insert i s ∧ ys ∈ subchain (insert i s) ∧ ∀ (b : α), b ∈ head? ys → y < b
⊢ False
[PROOFSTEP]
cases' chain'_iff_pairwise.mp h.1 with _ _ hy
[GOAL]
case a.cons.cons
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ (b : α), b ∈ s → i < b
h : y :: ys ∈ subchain (insert i s)
h' : y ∈ insert i s ∧ ys ∈ subchain (insert i s) ∧ ∀ (b : α), b ∈ head? ys → y < b
a✝ : List.Pairwise (fun x x_1 => x < x_1) ys
hy : ∀ (a' : α), a' ∈ ys → y < a'
⊢ False
[PROOFSTEP]
cases' h'.1 with h' h'
[GOAL]
case a.cons.cons.inl
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ (b : α), b ∈ s → i < b
h : y :: ys ∈ subchain (insert i s)
h'✝ : y ∈ insert i s ∧ ys ∈ subchain (insert i s) ∧ ∀ (b : α), b ∈ head? ys → y < b
a✝ : List.Pairwise (fun x x_1 => x < x_1) ys
hy : ∀ (a' : α), a' ∈ ys → y < a'
h' : y = i
⊢ False
case a.cons.cons.inr
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ (b : α), b ∈ s → i < b
h : y :: ys ∈ subchain (insert i s)
h'✝ : y ∈ insert i s ∧ ys ∈ subchain (insert i s) ∧ ∀ (b : α), b ∈ head? ys → y < b
a✝ : List.Pairwise (fun x x_1 => x < x_1) ys
hy : ∀ (a' : α), a' ∈ ys → y < a'
h' : y ∈ s
⊢ False
[PROOFSTEP]
exacts [(hy _ hi).ne h', not_le_of_gt (hy _ hi) (hx _ h').le]
[GOAL]
case a
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain (insert a s) ∧ length l + 1 ≤ length l' + 0
[PROOFSTEP]
intro l hl
[GOAL]
case a
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
l : List α
hl : l ∈ subchain s
⊢ ∃ l', l' ∈ subchain (insert a s) ∧ length l + 1 ≤ length l' + 0
[PROOFSTEP]
refine' ⟨a :: l, ⟨_, _⟩, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
l : List α
hl : l ∈ subchain s
⊢ length l + 1 ≤ length (a :: l) + 0
[PROOFSTEP]
simp
[GOAL]
case a.refine'_1
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
l : List α
hl : l ∈ subchain s
⊢ Chain' (fun x x_1 => x < x_1) (a :: l)
[PROOFSTEP]
rw [chain'_cons']
[GOAL]
case a.refine'_1
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
l : List α
hl : l ∈ subchain s
⊢ (∀ (y : α), y ∈ head? l → a < y) ∧ Chain' (fun x x_1 => x < x_1) l
[PROOFSTEP]
exact ⟨fun y hy ↦ hx _ (hl.2 _ (mem_of_mem_head? hy)), hl.1⟩
[GOAL]
case a.refine'_2
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
l : List α
hl : l ∈ subchain s
⊢ ∀ (i : α), i ∈ a :: l → i ∈ insert a s
[PROOFSTEP]
rintro x (_ | _)
[GOAL]
case a.refine'_2.head
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
l : List α
hl : l ∈ subchain s
⊢ a ∈ insert a s
case a.refine'_2.tail
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
l : List α
hl : l ∈ subchain s
x : α
a✝ : Mem x l
⊢ x ∈ insert a s
[PROOFSTEP]
exacts [Or.inl (Set.mem_singleton a), Or.inr (hl.2 x ‹_›)]
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
ha : ∀ (b : α), b ∈ s → b < a
⊢ chainHeight (insert a s) = chainHeight s + 1
[PROOFSTEP]
rw [← chainHeight_dual, ← chainHeight_dual s]
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
a : α
ha : ∀ (b : α), b ∈ s → b < a
⊢ chainHeight (↑ofDual ⁻¹' insert a s) = chainHeight (↑ofDual ⁻¹' s) + 1
[PROOFSTEP]
exact chainHeight_insert_of_forall_gt _ ha
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ chainHeight (s ∪ t) ≤ chainHeight s + chainHeight t
[PROOFSTEP]
classical
refine' iSup₂_le fun l hl ↦ _
let l₁ := l.filter (· ∈ s)
let l₂ := l.filter (· ∈ t)
have hl₁ : ↑l₁.length ≤ s.chainHeight :=
  by
  apply Set.length_le_chainHeight_of_mem_subchain
  exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
have hl₂ : ↑l₂.length ≤ t.chainHeight :=
  by
  apply Set.length_le_chainHeight_of_mem_subchain
  exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
refine' le_trans _ (add_le_add hl₁ hl₂)
simp_rw [← Nat.cast_add, ← Multiset.coe_card, ← Multiset.card_add, ← Multiset.coe_filter]
rw [Multiset.filter_add_filter, Multiset.filter_eq_self.mpr, Multiset.card_add, Nat.cast_add]
exacts [le_add_right rfl.le, hl.2]
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
⊢ chainHeight (s ∪ t) ≤ chainHeight s + chainHeight t
[PROOFSTEP]
refine' iSup₂_le fun l hl ↦ _
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
[PROOFSTEP]
let l₁ := l.filter (· ∈ s)
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
[PROOFSTEP]
let l₂ := l.filter (· ∈ t)
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
[PROOFSTEP]
have hl₁ : ↑l₁.length ≤ s.chainHeight :=
  by
  apply Set.length_le_chainHeight_of_mem_subchain
  exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ ↑(length l₁) ≤ chainHeight s
[PROOFSTEP]
apply Set.length_le_chainHeight_of_mem_subchain
[GOAL]
case hl
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
⊢ l₁ ∈ subchain s
[PROOFSTEP]
exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
i : α
h : i ∈ l₁
⊢ i ∈ s
[PROOFSTEP]
simpa using (of_mem_filter h : _)
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
[PROOFSTEP]
have hl₂ : ↑l₂.length ≤ t.chainHeight :=
  by
  apply Set.length_le_chainHeight_of_mem_subchain
  exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
⊢ ↑(length l₂) ≤ chainHeight t
[PROOFSTEP]
apply Set.length_le_chainHeight_of_mem_subchain
[GOAL]
case hl
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
⊢ l₂ ∈ subchain t
[PROOFSTEP]
exact ⟨hl.1.sublist (filter_sublist _), fun i h ↦ by simpa using (of_mem_filter h : _)⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
i : α
h : i ∈ l₂
⊢ i ∈ t
[PROOFSTEP]
simpa using (of_mem_filter h : _)
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(length l) ≤ chainHeight s + chainHeight t
[PROOFSTEP]
refine' le_trans _ (add_le_add hl₁ hl₂)
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(length l) ≤ ↑(length l₁) + ↑(length l₂)
[PROOFSTEP]
simp_rw [← Nat.cast_add, ← Multiset.coe_card, ← Multiset.card_add, ← Multiset.coe_filter]
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(↑Multiset.card ↑l) ≤ ↑(↑Multiset.card (Multiset.filter (fun b => b ∈ s) ↑l + Multiset.filter (fun b => b ∈ t) ↑l))
[PROOFSTEP]
rw [Multiset.filter_add_filter, Multiset.filter_eq_self.mpr, Multiset.card_add, Nat.cast_add]
[GOAL]
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ↑(↑Multiset.card ↑l) ≤ ↑(↑Multiset.card ↑l) + ↑(↑Multiset.card (Multiset.filter (fun a => a ∈ s ∧ a ∈ t) ↑l))
α : Type u_1
β : Type u_2
s t : Set α
inst✝ : Preorder α
l : List α
hl : l ∈ subchain (s ∪ t)
l₁ : List α := filter (fun x => decide (x ∈ s)) l
l₂ : List α := filter (fun x => decide (x ∈ t)) l
hl₁ : ↑(length l₁) ≤ chainHeight s
hl₂ : ↑(length l₂) ≤ chainHeight t
⊢ ∀ (a : α), a ∈ ↑l → a ∈ s ∨ a ∈ t
[PROOFSTEP]
exacts [le_add_right rfl.le, hl.2]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
inst✝ : Preorder α
s t : Set α
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a < b
⊢ chainHeight (s ∪ t) = chainHeight s + chainHeight t
[PROOFSTEP]
cases h : t.chainHeight
[GOAL]
case none
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [WithTop.none_eq_top, add_top, eq_top_iff, ← WithTop.none_eq_top, ← h]
[GOAL]
case none
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact Set.chainHeight_mono (Set.subset_union_right _ _)
[GOAL]
case some
α : Type u_1
β : Type u_2
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✝
[PROOFSTEP]
apply le_antisymm
[GOAL]
case some.a
α : Type u_1
β : Type u_2
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✝
[PROOFSTEP]
rw [← h]
[GOAL]
case some.a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact chainHeight_union_le
[GOAL]
case some.a
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
rw [WithTop.some_eq_coe, ← add_zero (s ∪ t).chainHeight, ← WithTop.coe_zero, ENat.some_eq_coe,
  chainHeight_add_le_chainHeight_add]
[GOAL]
case some.a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
intro l hl
[GOAL]
case some.a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain ⟨l', hl', rfl⟩ := exists_chain_of_le_chainHeight t h.symm.le
[GOAL]
case some.a.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
refine' ⟨l ++ l', ⟨Chain'.append hl.1 hl'.1 fun x hx y hy ↦ _, fun i hi ↦ _⟩, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp
[GOAL]
case some.a.intro.intro.refine'_1
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact H x (hl.2 _ <| mem_of_mem_getLast? hx) y (hl'.2 _ <| mem_of_mem_head? hy)
[GOAL]
case some.a.intro.intro.refine'_2
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [mem_append] at hi 
[GOAL]
case some.a.intro.intro.refine'_2
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
cases' hi with hi hi
[GOAL]
case some.a.intro.intro.refine'_2.inl
α : Type u_1
β : Type u_2
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_2
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
[PROOFSTEP]
exacts [Or.inl (hl.2 _ hi), Or.inr (hl'.2 _ hi)]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
⊢ WellFoundedGT ↑s
[PROOFSTEP]
haveI : IsTrans { x // x ∈ s } (↑· < ↑·) := inferInstance
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
⊢ WellFoundedGT ↑s
[PROOFSTEP]
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 hs
[GOAL]
case intro
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
⊢ WellFoundedGT ↑s
[PROOFSTEP]
refine' ⟨RelEmbedding.wellFounded_iff_no_descending_seq.2 ⟨fun f ↦ _⟩⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ False
[PROOFSTEP]
refine' n.lt_succ_self.not_le (WithTop.coe_le_coe.1 <| hn.symm ▸ _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ chainHeight s
[PROOFSTEP]
refine'
  le_iSup₂_of_le _
    ⟨chain'_map_of_chain' ((↑) : { x // x ∈ s } → α) (fun _ _ ↦ id)
        (chain'_iff_pairwise.2 <| pairwise_ofFn.2 fun i j ↦ f.map_rel_iff.2),
      fun i h ↦ _⟩
    _
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ℕ
[PROOFSTEP]
exact n.succ
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
i : α
h : i ∈ map Subtype.val (ofFn fun i => ↑f ↑i)
⊢ i ∈ s
[PROOFSTEP]
obtain ⟨a, -, rfl⟩ := mem_map.1 h
[GOAL]
case intro.refine'_2.intro.intro
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
a : { x // x ∈ s }
h : ↑a ∈ map Subtype.val (ofFn fun i => ↑f ↑i)
⊢ ↑a ∈ s
[PROOFSTEP]
exact a.prop
[GOAL]
case intro.refine'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ ↑(length (map Subtype.val (ofFn fun i => ↑f ↑i)))
[PROOFSTEP]
rw [length_map, length_ofFn]
[GOAL]
case intro.refine'_3
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1
n : ℕ
hn : ↑n = chainHeight s
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑(Nat.succ n) ≤ ↑(Nat.succ n)
[PROOFSTEP]
exact le_rfl
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Set α
inst✝ : Preorder α
s : Set α
hs : chainHeight s ≠ ⊤
⊢ chainHeight (↑ofDual ⁻¹' s) ≠ ⊤
[PROOFSTEP]
rwa [chainHeight_dual]
