-- Mathlib/Order/Height.lean
theorem chainHeight_insert_of_forall_gt (a : α) (hx : ∀ b ∈ s, a < b) :
    (insert a s).chainHeight = s.chainHeight + 1

Proof state:
case a.refine_1
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ Chain' (fun x1 x2 => x1 < x2) (a :: l)

Tactic:
rw [chain'_cons']

Result:
case a.refine_1
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ (∀ y ∈ l.head?, a < y) ∧ Chain' (fun x1 x2 => x1 < x2) l

Proof state:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ ∀ l ∈ s.subchain, ∃ l' ∈ (insert a s).subchain, l.length + 1 ≤ l'.length + 0

Tactic:
intro l hl

Result:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ ∃ l' ∈ (insert a s).subchain, l.length + 1 ≤ l'.length + 0

Proof state:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ ∀ l ∈ (insert a s).subchain, ∃ l' ∈ s.subchain, l.length + 0 ≤ l'.length + 1

Tactic:
rintro (_ | ⟨y, ys⟩) h

Result:
case a.nil
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
h : [] ∈ (insert a s).subchain
⊢ ∃ l' ∈ s.subchain, [].length + 0 ≤ l'.length + 1

case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
⊢ ∃ l' ∈ s.subchain, (y :: ys).length + 0 ≤ l'.length + 1

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ (insert a s).chainHeight + ↑0 = s.chainHeight + ↑1

Tactic:
apply le_antisymm <;> rw [chainHeight_add_le_chainHeight_add]

Result:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ ∀ l ∈ (insert a s).subchain, ∃ l' ∈ s.subchain, l.length + 0 ≤ l'.length + 1

case a
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ ∀ l ∈ s.subchain, ∃ l' ∈ (insert a s).subchain, l.length + 1 ≤ l'.length + 0

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ (insert a s).chainHeight = s.chainHeight + 1

Tactic:
rw [← add_zero (insert a s).chainHeight]

Result:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ (insert a s).chainHeight + 0 = s.chainHeight + 1

Proof state:
case a.refine_2
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ ∀ i ∈ a :: l, i ∈ insert a s

Tactic:
rintro x (_ | _)

Result:
case a.refine_2.head
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ a ∈ insert a s

case a.refine_2.tail
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
x : α
a✝ : Mem x l
⊢ x ∈ insert a s

Proof state:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
h' : y ∈ insert a s ∧ ys ∈ (insert a s).subchain ∧ ∀ b ∈ ys.head?, y < b
⊢ ∃ l' ∈ s.subchain, (y :: ys).length + 0 ≤ l'.length + 1

Tactic:
refine ⟨ys, ⟨h'.2.1.1, fun i hi ↦ ?_⟩, by simp⟩

Result:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
h' : y ∈ insert a s ∧ ys ∈ (insert a s).subchain ∧ ∀ b ∈ ys.head?, y < b
i : α
hi : i ∈ ys
⊢ i ∈ s

Proof state:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ b ∈ s, i < b
h : y :: ys ∈ (insert i s).subchain
h' : y ∈ insert i s ∧ ys ∈ (insert i s).subchain ∧ ∀ b ∈ ys.head?, y < b
⊢ False

Tactic:
obtain - | hy := chain'_iff_pairwise.mp h.1

Result:
case a.cons.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ b ∈ s, i < b
h : y :: ys ∈ (insert i s).subchain
h' : y ∈ insert i s ∧ ys ∈ (insert i s).subchain ∧ ∀ b ∈ ys.head?, y < b
a✝ : List.Pairwise (fun x1 x2 => x1 < x2) ys
hy : ∀ a' ∈ ys, y < a'
⊢ False

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ (insert a s).chainHeight + 0 = s.chainHeight + 1

Tactic:
change (insert a s).chainHeight + (0 : ℕ) = s.chainHeight + (1 : ℕ)

Result:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
⊢ (insert a s).chainHeight + ↑0 = s.chainHeight + ↑1

Proof state:
case a.cons.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ b ∈ s, i < b
h : y :: ys ∈ (insert i s).subchain
h' : y ∈ insert i s ∧ ys ∈ (insert i s).subchain ∧ ∀ b ∈ ys.head?, y < b
a✝ : List.Pairwise (fun x1 x2 => x1 < x2) ys
hy : ∀ a' ∈ ys, y < a'
⊢ False

Tactic:
rcases h'.1 with h' | h'

Result:
case a.cons.cons.inl
α : Type u_1
s : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ b ∈ s, i < b
h : y :: ys ∈ (insert i s).subchain
h'✝ : y ∈ insert i s ∧ ys ∈ (insert i s).subchain ∧ ∀ b ∈ ys.head?, y < b
a✝ : List.Pairwise (fun x1 x2 => x1 < x2) ys
hy : ∀ a' ∈ ys, y < a'
h' : y = i
⊢ False

case a.cons.cons.inr
α : Type u_1
s : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ b ∈ s, i < b
h : y :: ys ∈ (insert i s).subchain
h'✝ : y ∈ insert i s ∧ ys ∈ (insert i s).subchain ∧ ∀ b ∈ ys.head?, y < b
a✝ : List.Pairwise (fun x1 x2 => x1 < x2) ys
hy : ∀ a' ∈ ys, y < a'
h' : y ∈ s
⊢ False

Proof state:
case a.refine_1
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ (∀ y ∈ l.head?, a < y) ∧ Chain' (fun x1 x2 => x1 < x2) l

Tactic:
exact ⟨fun y hy ↦ hx _ (hl.2 _ (mem_of_mem_head? hy)), hl.1⟩

Result:
no goals

Proof state:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
h' : y ∈ insert a s ∧ ys ∈ (insert a s).subchain ∧ ∀ b ∈ ys.head?, y < b
i : α
hi : i ∈ ys
⊢ ¬i = a

Tactic:
rintro rfl

Result:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ b ∈ s, i < b
h : y :: ys ∈ (insert i s).subchain
h' : y ∈ insert i s ∧ ys ∈ (insert i s).subchain ∧ ∀ b ∈ ys.head?, y < b
⊢ False

Proof state:
case a
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ ∃ l' ∈ (insert a s).subchain, l.length + 1 ≤ l'.length + 0

Tactic:
refine ⟨a::l, ⟨?_, ?_⟩, by simp⟩

Result:
case a.refine_1
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ Chain' (fun x1 x2 => x1 < x2) (a :: l)

case a.refine_2
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ ∀ i ∈ a :: l, i ∈ insert a s

Proof state:
case a.cons.cons.inl
α : Type u_1
s : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ b ∈ s, i < b
h : y :: ys ∈ (insert i s).subchain
h'✝ : y ∈ insert i s ∧ ys ∈ (insert i s).subchain ∧ ∀ b ∈ ys.head?, y < b
a✝ : List.Pairwise (fun x1 x2 => x1 < x2) ys
hy : ∀ a' ∈ ys, y < a'
h' : y = i
⊢ False

case a.cons.cons.inr
α : Type u_1
s : Set α
inst✝ : Preorder α
y : α
ys : List α
i : α
hi : i ∈ ys
hx : ∀ b ∈ s, i < b
h : y :: ys ∈ (insert i s).subchain
h'✝ : y ∈ insert i s ∧ ys ∈ (insert i s).subchain ∧ ∀ b ∈ ys.head?, y < b
a✝ : List.Pairwise (fun x1 x2 => x1 < x2) ys
hy : ∀ a' ∈ ys, y < a'
h' : y ∈ s
⊢ False

Tactic:
exacts [(hy _ hi).ne h', not_le_of_gt (hy _ hi) (hx _ h').le]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ l.length + 1 ≤ (a :: l).length + 0

Tactic:
simp

Result:
no goals

Proof state:
case a.refine_2.head
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
⊢ a ∈ insert a s

case a.refine_2.tail
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
l : List α
hl : l ∈ s.subchain
x : α
a✝ : Mem x l
⊢ x ∈ insert a s

Tactic:
exacts [Or.inl (Set.mem_singleton a), Or.inr (hl.2 x ‹_›)]

Result:
no goals