[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]


[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
by_cases h : ∃ b, (a, b) ∈ f.val
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ∃ b, (a, b) ∈ ↑f
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
cases' h with b hb
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
b : β
hb : (a, b) ∈ ↑f
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
exact ⟨b, fun p hp ↦ f.prop _ hp _ hb⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
have :
  ∀ x ∈ (f.val.filter fun p : α × β ↦ p.fst < a).image Prod.snd,
    ∀ y ∈ (f.val.filter fun p : α × β ↦ a < p.fst).image Prod.snd, x < y :=
  by
  intro x hx y hy
  rw [Finset.mem_image] at hx hy
  rcases hx with ⟨p, hp1, rfl⟩
  rcases hy with ⟨q, hq1, rfl⟩
  rw [Finset.mem_filter] at hp1 hq1
  rw [← lt_iff_lt_of_cmp_eq_cmp (f.prop _ hp1.1 _ hq1.1)]
  exact lt_trans hp1.right hq1.right
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
⊢ ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
[PROOFSTEP]
intro x hx y hy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
x : β
hx : x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f)
y : β
hy : y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f)
⊢ x < y
[PROOFSTEP]
rw [Finset.mem_image] at hx hy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
x : β
hx : ∃ a_1, a_1 ∈ Finset.filter (fun p => p.fst < a) ↑f ∧ a_1.snd = x
y : β
hy : ∃ a_1, a_1 ∈ Finset.filter (fun p => a < p.fst) ↑f ∧ a_1.snd = y
⊢ x < y
[PROOFSTEP]
rcases hx with ⟨p, hp1, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
y : β
hy : ∃ a_1, a_1 ∈ Finset.filter (fun p => a < p.fst) ↑f ∧ a_1.snd = y
p : α × β
hp1 : p ∈ Finset.filter (fun p => p.fst < a) ↑f
⊢ p.snd < y
[PROOFSTEP]
rcases hy with ⟨q, hq1, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
p : α × β
hp1 : p ∈ Finset.filter (fun p => p.fst < a) ↑f
q : α × β
hq1 : q ∈ Finset.filter (fun p => a < p.fst) ↑f
⊢ p.snd < q.snd
[PROOFSTEP]
rw [Finset.mem_filter] at hp1 hq1
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
p : α × β
hp1 : p ∈ ↑f ∧ p.fst < a
q : α × β
hq1 : q ∈ ↑f ∧ a < q.fst
⊢ p.snd < q.snd
[PROOFSTEP]
rw [← lt_iff_lt_of_cmp_eq_cmp (f.prop _ hp1.1 _ hq1.1)]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
p : α × β
hp1 : p ∈ ↑f ∧ p.fst < a
q : α × β
hq1 : q ∈ ↑f ∧ a < q.fst
⊢ p.fst < q.fst
[PROOFSTEP]
exact lt_trans hp1.right hq1.right
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
cases' exists_between_finsets _ _ this with b hb
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
⊢ ∃ b, ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
use b
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
⊢ ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
[PROOFSTEP]
rintro ⟨p1, p2⟩ hp
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
have : p1 ≠ a := fun he ↦ h ⟨p2, he ▸ hp⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
cases' lt_or_gt_of_ne this with hl hr
[GOAL]
case h.mk.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hl : p1 < a
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
have : p1 < a ∧ p2 < b := ⟨hl, hb.1 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hl⟩, rfl⟩)⟩
[GOAL]
case h.mk.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hl : p1 < a
this : p1 < a ∧ p2 < b
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff] at this
[GOAL]
case h.mk.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hl : p1 < a
this : cmp p1 a = Ordering.lt ∧ cmp p2 b = Ordering.lt
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
exact this.1.trans this.2.symm
[GOAL]
case h.mk.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hr : p1 > a
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
have : a < p1 ∧ b < p2 := ⟨hr, hb.2 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hr⟩, rfl⟩)⟩
[GOAL]
case h.mk.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hr : p1 > a
this : a < p1 ∧ b < p2
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
rw [← cmp_eq_gt_iff, ← cmp_eq_gt_iff] at this
[GOAL]
case h.mk.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ :
  ∀ (x : β),
    x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) →
      ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → x < y
b : β
hb :
  (∀ (x : β), x ∈ Finset.image Prod.snd (Finset.filter (fun p => p.fst < a) ↑f) → x < b) ∧
    ∀ (y : β), y ∈ Finset.image Prod.snd (Finset.filter (fun p => a < p.fst) ↑f) → b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hr : p1 > a
this : cmp p1 a = Ordering.gt ∧ cmp p2 b = Ordering.gt
⊢ cmp (p1, p2).fst a = cmp (p1, p2).snd b
[PROOFSTEP]
exact this.1.trans this.2.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd
p : β × α
hp : p ∈ Finset.image (↑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ Finset.image (↑(Equiv.prodComm α β)) f
⊢ ↑(Equiv.prodComm α β).symm p ∈ f
[PROOFSTEP]
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage] at hp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd
p : β × α
hp : p ∈ ↑(Equiv.prodComm α β).symm ⁻¹' ↑f
q : β × α
hq : q ∈ Finset.image (↑(Equiv.prodComm α β)) f
⊢ ↑(Equiv.prodComm α β).symm p ∈ f
[PROOFSTEP]
rwa [← Finset.mem_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd
p : β × α
hp : p ∈ Finset.image (↑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ Finset.image (↑(Equiv.prodComm α β)) f
⊢ ↑(Equiv.prodComm α β).symm q ∈ f
[PROOFSTEP]
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage] at hq
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd
p : β × α
hp : p ∈ Finset.image (↑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ ↑(Equiv.prodComm α β).symm ⁻¹' ↑f
⊢ ↑(Equiv.prodComm α β).symm q ∈ f
[PROOFSTEP]
rwa [← Finset.mem_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
⊢ ∃ y, y ∈ {f | ∃ b, (a, b) ∈ ↑f} ∧ f ≤ y
[PROOFSTEP]
cases' exists_across f a with b a_b
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
⊢ ∃ y, y ∈ {f | ∃ b, (a, b) ∈ ↑f} ∧ f ≤ y
[PROOFSTEP]
refine ⟨⟨insert (a, b) f.val, fun p hp q hq ↦ ?_⟩, ⟨b, Finset.mem_insert_self _ _⟩, Finset.subset_insert _ _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p : α × β
hp : p ∈ insert (a, b) ↑f
q : α × β
hq : q ∈ insert (a, b) ↑f
⊢ cmp p.fst q.fst = cmp p.snd q.snd
[PROOFSTEP]
rw [Finset.mem_insert] at hp hq
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p : α × β
hp : p = (a, b) ∨ p ∈ ↑f
q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
⊢ cmp p.fst q.fst = cmp p.snd q.snd
[PROOFSTEP]
rcases hp with (rfl | pf)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
⊢ cmp (a, b).fst q.fst = cmp (a, b).snd q.snd
[PROOFSTEP]
rcases hq with (rfl | qf)
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
pf : p ∈ ↑f
⊢ cmp p.fst q.fst = cmp p.snd q.snd
[PROOFSTEP]
rcases hq with (rfl | qf)
[GOAL]
case intro.inl.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
⊢ cmp (a, b).fst (a, b).fst = cmp (a, b).snd (a, b).snd
[PROOFSTEP]
simp only [cmp_self_eq_eq]
[GOAL]
case intro.inl.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
q : α × β
qf : q ∈ ↑f
⊢ cmp (a, b).fst q.fst = cmp (a, b).snd q.snd
[PROOFSTEP]
rw [cmp_eq_cmp_symm]
[GOAL]
case intro.inl.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
q : α × β
qf : q ∈ ↑f
⊢ cmp q.fst (a, b).fst = cmp q.snd (a, b).snd
[PROOFSTEP]
exact a_b _ qf
[GOAL]
case intro.inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p : α × β
pf : p ∈ ↑f
⊢ cmp p.fst (a, b).fst = cmp p.snd (a, b).snd
[PROOFSTEP]
exact a_b _ pf
[GOAL]
case intro.inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ (p : α × β), p ∈ ↑f → cmp p.fst a = cmp p.snd b
p q : α × β
pf : p ∈ ↑f
qf : q ∈ ↑f
⊢ cmp p.fst q.fst = cmp p.snd q.snd
[PROOFSTEP]
exact f.prop _ pf _ qf
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
⊢ ∃ y, y ∈ {f | ∃ a, (a, b) ∈ ↑f} ∧ f ≤ y
[PROOFSTEP]
rcases(definedAtLeft α b).mem_gt f.comm with ⟨f', ⟨a, ha⟩, hl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ∃ y, y ∈ {f | ∃ a, (a, b) ∈ ↑f} ∧ f ≤ y
[PROOFSTEP]
refine' ⟨f'.comm, ⟨a, _⟩, _⟩
[GOAL]
case intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ (a, b) ∈ ↑(PartialIso.comm f')
[PROOFSTEP]
change (a, b) ∈ f'.val.image _
[GOAL]
case intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ (a, b) ∈ Finset.image ↑(Equiv.prodComm β α) ↑f'
[PROOFSTEP]
rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage]
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ f ≤ PartialIso.comm f'
[PROOFSTEP]
change _ ⊆ f'.val.image _
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : PartialIso.comm f ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ (fun a => ↑a) f ⊆ Finset.image ↑(Equiv.prodComm β α) ↑f'
[PROOFSTEP]
rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.subset_image, ← Finset.coe_image, Finset.coe_subset]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
rcases exists_pair_lt β with ⟨x, y, hxy⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
cases' exists_between hxy with a ha
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
haveI : Nonempty (Set.Ioo x y) := ⟨⟨a, ha⟩⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
let our_ideal : Ideal (PartialIso α _) := idealOfCofinals default (definedAtLeft (Set.Ioo x y))
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
let F a := funOfIdeal a our_ideal (cofinal_meets_idealOfCofinals _ _ a)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
⊢ Nonempty (α ↪o β)
[PROOFSTEP]
refine ⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_) (OrderEmbedding.subtype _)⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
a₁ a₂ : α
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
[PROOFSTEP]
rcases(F a₁).prop with ⟨f, hf, ha₁⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
a₁ a₂ : α
f : PartialIso α ↑(Set.Ioo x y)
hf : f ∈ our_ideal
ha₁ : (a₁, ↑(F a₁)) ∈ ↑f
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
[PROOFSTEP]
rcases(F a₂).prop with ⟨g, hg, ha₂⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
a₁ a₂ : α
f : PartialIso α ↑(Set.Ioo x y)
hf : f ∈ our_ideal
ha₁ : (a₁, ↑(F a₁)) ∈ ↑f
g : PartialIso α ↑(Set.Ioo x y)
hg : g ∈ our_ideal
ha₂ : (a₂, ↑(F a₂)) ∈ ↑g
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
[PROOFSTEP]
rcases our_ideal.directed _ hf _ hg with ⟨m, _hm, fm, gm⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Encodable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a =>
    funOfIdeal a our_ideal
      (_ : ∃ x_1, x_1 ∈ definedAtLeft (↑(Set.Ioo x y)) a ∧ x_1 ∈ idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y)))
a₁ a₂ : α
f : PartialIso α ↑(Set.Ioo x y)
hf : f ∈ our_ideal
ha₁ : (a₁, ↑(F a₁)) ∈ ↑f
g : PartialIso α ↑(Set.Ioo x y)
hg : g ∈ our_ideal
ha₂ : (a₂, ↑(F a₂)) ∈ ↑g
m : PartialIso α ↑(Set.Ioo x y)
_hm : m ∈ ↑our_ideal
fm : f ≤ m
gm : g ≤ m
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
[PROOFSTEP]
exact (lt_iff_lt_of_cmp_eq_cmp <| m.prop (a₁, _) (fm ha₁) (a₂, _) (gm ha₂)).mp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Encodable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Encodable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a => funOfIdeal a our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inl a) ∧ x ∈ idealOfCofinals default to_cofinal)
G : (b : β) → { a // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun b => invOfIdeal b our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inr b) ∧ x ∈ idealOfCofinals default to_cofinal)
a : α
b : β
⊢ cmp a ((fun b => ↑(G b)) b) = cmp ((fun a => ↑(F a)) a) b
[PROOFSTEP]
rcases(F a).prop with ⟨f, hf, ha⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Encodable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Encodable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a => funOfIdeal a our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inl a) ∧ x ∈ idealOfCofinals default to_cofinal)
G : (b : β) → { a // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun b => invOfIdeal b our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inr b) ∧ x ∈ idealOfCofinals default to_cofinal)
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, ↑(F a)) ∈ ↑f
⊢ cmp a ((fun b => ↑(G b)) b) = cmp ((fun a => ↑(F a)) a) b
[PROOFSTEP]
rcases(G b).prop with ⟨g, hg, hb⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Encodable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Encodable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a => funOfIdeal a our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inl a) ∧ x ∈ idealOfCofinals default to_cofinal)
G : (b : β) → { a // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun b => invOfIdeal b our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inr b) ∧ x ∈ idealOfCofinals default to_cofinal)
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, ↑(F a)) ∈ ↑f
g : PartialIso α β
hg : g ∈ our_ideal
hb : (↑(G b), b) ∈ ↑g
⊢ cmp a ((fun b => ↑(G b)) b) = cmp ((fun a => ↑(F a)) a) b
[PROOFSTEP]
rcases our_ideal.directed _ hf _ hg with ⟨m, _, fm, gm⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Encodable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Encodable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun a => funOfIdeal a our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inl a) ∧ x ∈ idealOfCofinals default to_cofinal)
G : (b : β) → { a // ∃ f, f ∈ our_ideal ∧ (a, b) ∈ ↑f } :=
  fun b => invOfIdeal b our_ideal (_ : ∃ x, x ∈ to_cofinal (Sum.inr b) ∧ x ∈ idealOfCofinals default to_cofinal)
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, ↑(F a)) ∈ ↑f
g : PartialIso α β
hg : g ∈ our_ideal
hb : (↑(G b), b) ∈ ↑g
m : PartialIso α β
left✝ : m ∈ ↑our_ideal
fm : f ≤ m
gm : g ≤ m
⊢ cmp a ((fun b => ↑(G b)) b) = cmp ((fun a => ↑(F a)) a) b
[PROOFSTEP]
exact m.prop (a, _) (fm ha) (_, b) (gm hb)