English
If a is greater than every element of s, then inserting a into s increases chainHeight by 1.
Русский
Если a больше любого элемента s, добавление a в s увеличивает цепную высоту на 1.
LaTeX
$$∀ {s : Set α} [Preorder α] (a : α) (hx : ∀ b ∈ s, a > b), (insert a s).chainHeight = s.chainHeight + 1$$
Lean4
theorem chainHeight_insert_of_forall_gt (a : α) (hx : ∀ b ∈ s, a < b) : (insert a s).chainHeight = s.chainHeight + 1 :=
by
rw [← add_zero (insert a s).chainHeight]
change (insert a s).chainHeight + (0 : ℕ) = s.chainHeight + (1 : ℕ)
apply le_antisymm <;> rw [chainHeight_add_le_chainHeight_add]
· rintro (_ | ⟨y, ys⟩) h
· exact ⟨[], nil_mem_subchain _, zero_le _⟩
· have h' := cons_mem_subchain_iff.mp h
refine ⟨ys, ⟨h'.2.1.1, fun i hi ↦ ?_⟩, by simp⟩
apply (h'.2.1.2 i hi).resolve_left
rintro rfl
obtain - | hy := isChain_iff_pairwise.mp h.1
rcases h'.1 with h' | h'
exacts [(hy _ hi).ne h', not_le_of_gt (hy _ hi) (hx _ h').le]
· intro l hl
refine ⟨a :: l, ⟨?_, ?_⟩, by simp⟩
· rw [isChain_cons']
exact ⟨fun y hy ↦ hx _ (hl.2 _ (mem_of_mem_head? hy)), hl.1⟩
· rintro x (_ | _)
exacts [Or.inl (Set.mem_singleton a), Or.inr (hl.2 x ‹x ∈ l›)]
