English
Let s and t be finite subsets of a linearly ordered set with s ≤ t in colex and |s| ≤ |t|. If a is an element of s, then the colex order of s with a removed is bounded above by the colex order of t with a suitable minimal element of t removed, i.e., toColex(s \ {a}) ≤ toColex(t \ {min' t}).
Русский
Пусть s,t — конечные подмножества множества с линейно упорядоченным элементами, причём s ≤ t в колексическом порядке и |s| ≤ |t|. При любом a ∈ s выполняется, что колексальный порядок для s без элемента a не превосходит колексального порядка для t без подходящего минимального элемента t, то есть toColex(s \ {a}) ≤ toColex(t \ {min' t}).
LaTeX
$$$\forall s,t\; (s \le_{Colex} t) \land (|s| \le |t|) \land a \in s \Rightarrow toColex\,(s\setminus\{a\}) \le toColex\,(t\setminus\min' t).$$$
Lean4
/-- If `s ≤ t` in colex and `#s ≤ #t`, then `s \ {a} ≤ t \ {min t}` for any `a ∈ s`. -/
theorem erase_le_erase_min' (hst : toColex s ≤ toColex t) (hcard : #s ≤ #t) (ha : a ∈ s) :
toColex (s.erase a) ≤ toColex (t.erase <| min' t <| card_pos.1 <| (card_pos.2 ⟨a, ha⟩).trans_le hcard) :=
by
generalize_proofs ht
set m := min' t ht
obtain rfl | h' := eq_or_ne s t
· exact (erase_le_erase ha <| min'_mem _ _).2 <| min'_le _ _ <| ha
replace hst := hst.lt_of_ne <| toColex_inj.not.2 h'
simp only [lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc] at hst
obtain ⟨w, hwt, hws, hw⟩ := hst
obtain hwa | haw := (ne_of_mem_of_not_mem ha hws).symm.lt_or_gt
· have hma : m < a := (min'_le _ _ hwt).trans_lt hwa
refine
(lt_iff_exists_forall_lt.2 ⟨a, mem_erase.2 ⟨hma.ne', (hw hwa).1 ha⟩, notMem_erase _ _, fun b hbs hbt ↦ ?_⟩).le
change b ∉ t.erase m at hbt
rw [mem_erase, not_and_or, not_ne_iff] at hbt
obtain rfl | hbt := hbt
· assumption
· by_contra! hab
exact hbt <| (hw <| hwa.trans_le hab).1 <| mem_of_mem_erase hbs
obtain rfl | hmw : m = w ∨ m < w := (min'_le _ _ hwt).eq_or_lt
· have : erase t m ⊆ erase s a := by
rintro b hb
rw [mem_erase] at hb ⊢
exact ⟨(haw.trans_le <| min'_le _ _ hb.2).ne', (hw <| hb.1.lt_of_le' <| min'_le _ _ hb.2).2 hb.2⟩
rw [eq_of_subset_of_card_le this]
rw [card_erase_of_mem ha, card_erase_of_mem (min'_mem _ _)]
exact
tsub_le_tsub_right hcard
_
-- If `m < w`, then `w` works as the colex witness for `s \ {a} < t \ {m}`
· refine (lt_iff_exists_forall_lt.2 ⟨w, mem_erase.2 ⟨hmw.ne', hwt⟩, mt mem_of_mem_erase hws, fun b hbs hbt ↦ ?_⟩).le
change b ∉ t.erase m at hbt
rw [mem_erase, not_and_or, not_ne_iff] at hbt
obtain rfl | hbt := hbt
· assumption
· by_contra! hwb
exact hbt <| (hw <| hwb.lt_of_ne <| ne_of_mem_of_not_mem hwt hbt).1 <| mem_of_mem_erase hbs
