α : Type u_1
β : Type ?u.34460
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) + 0 = chainHeight s + 1
α : Type u_1
β : Type ?u.34460
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) = chainHeight s + 1
rw [← add_zero (insert a s).chainHeight]
α : Type u_1
β : Type ?u.34460
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) + ↑0 = chainHeight s + ↑1
α : Type u_1
β : Type ?u.34460
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) + 0 = chainHeight s + 1
change (insert a s).chainHeight + (0 : ℕ) = s.chainHeight + (1 : ℕ)
case a
α : Type u_1
β : Type ?u.34460
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

case a
α : Type u_1
β : Type ?u.34460
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
α : Type u_1
β : Type ?u.34460
s t : Set α
inst✝ : Preorder α
a : α
hx : ∀ (b : α), b ∈ s → a < b
⊢ chainHeight (insert a s) + ↑0 = chainHeight s + ↑1
apply le_antisymm <;> rw [chainHeight_add_le_chainHeight_add]
case a.nil
α : Type u_1
β : Type ?u.34460
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

case a.cons
α : Type u_1
β : Type ?u.34460
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
case a
α : Type u_1
β : Type ?u.34460
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
rintro (_ | ⟨y, ys⟩) h
no goals
case a.nil
α : Type u_1
β : Type ?u.34460
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
exact ⟨[], nil_mem_subchain _, zero_le _⟩
case a.cons
α : Type u_1
β : Type ?u.34460
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
case a.cons
α : Type u_1
β : Type ?u.34460
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
have h' := cons_mem_subchain_iff.mp h
case a.cons
α : Type u_1
β : Type ?u.34460
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
case a.cons
α : Type u_1
β : Type ?u.34460
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
refine' ⟨ys, ⟨h'.2.1.1, fun i hi ↦ _⟩, by simp⟩
case a.cons
α : Type u_1
β : Type ?u.34460
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
case a.cons
α : Type u_1
β : Type ?u.34460
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
apply (h'.2.1.2 i hi).resolve_left
case a.cons
α : Type u_1
β : Type ?u.34460
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
case a.cons
α : Type u_1
β : Type ?u.34460
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
rintro rfl
case a.cons.cons
α : Type u_1
β : Type ?u.34460
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
case a.cons
α : Type u_1
β : Type ?u.34460
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
cases' chain'_iff_pairwise.mp h.1 with _ _ hy
case a.cons.cons.inl
α : Type u_1
β : Type ?u.34460
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.34460
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
case a.cons.cons
α : Type u_1
β : Type ?u.34460
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
cases' h'.1 with h' h'
no goals
case a.cons.cons.inl
α : Type u_1
β : Type ?u.34460
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.34460
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
exacts [(hy _ hi).ne h', not_le_of_gt (hy _ hi) (hx _ h').le]
no goals
α : Type u_1
β : Type ?u.34460
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
simp
case a
α : Type u_1
β : Type ?u.34460
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
case a
α : Type u_1
β : Type ?u.34460
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
intro l hl
case a.refine'_1
α : Type u_1
β : Type ?u.34460
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)

case a.refine'_2
α : Type u_1
β : Type ?u.34460
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
case a
α : Type u_1
β : Type ?u.34460
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
refine' ⟨a::l, ⟨_, _⟩, by simp⟩
no goals
α : Type u_1
β : Type ?u.34460
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
simp
case a.refine'_1
α : Type u_1
β : Type ?u.34460
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
case a.refine'_1
α : Type u_1
β : Type ?u.34460
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)
rw [chain'_cons']
no goals
case a.refine'_1
α : Type u_1
β : Type ?u.34460
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
exact ⟨fun y hy ↦ hx _ (hl.2 _ (mem_of_mem_head? hy)), hl.1⟩
case a.refine'_2.head
α : Type u_1
β : Type ?u.34460
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.34460
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
case a.refine'_2
α : Type u_1
β : Type ?u.34460
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
rintro x (_ | _)
no goals
case a.refine'_2.head
α : Type u_1
β : Type ?u.34460
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.34460
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
exacts [Or.inl (Set.mem_singleton a), Or.inr (hl.2 x ‹_›)]