English
Erasing after inserting into the erased list recovers the original list.
Русский
После вставки в список последующее стирание восстанавливает исходный список.
LaTeX
$$$$ (xs.\erase x).\operatorname{orderedInsert}(r,x) = xs. $$$$
Lean4
/-- For an antisymmetric relation, erasing then inserting is the identity. -/
theorem orderedInsert_erase [DecidableEq α] [IsAntisymm α r] (x : α) (xs : List α) (hx : x ∈ xs) (hxs : Sorted r xs) :
(xs.erase x).orderedInsert r x = xs := by
induction xs generalizing x with
| nil => cases hx
| cons y ys ih =>
rw [sorted_cons] at hxs
obtain rfl | hxy := Decidable.eq_or_ne x y
· rw [erase_cons_head]
cases ys with
| nil => rfl
| cons z zs => rw [orderedInsert, if_pos (hxs.1 _ (.head zs))]
· rw [mem_cons] at hx
replace hx := hx.resolve_left hxy
rw [erase_cons_tail (not_beq_of_ne hxy.symm), orderedInsert, ih _ hx hxs.2, if_neg]
refine mt (fun hrxy => ?_) hxy
exact antisymm hrxy (hxs.1 _ hx)
