English
The last element of the sorted list equals the maximum auxiliary value.
Русский
Последний элемент отсортированного списка равен максимальному вспомогательному значению.
LaTeX
$$$ (s.sort (\\le))[(s.sort (\\le)).length - 1] = s.max' H $$$
Lean4
theorem sorted_last_eq_max'_aux (s : Finset α) (h : (s.sort (· ≤ ·)).length - 1 < (s.sort (· ≤ ·)).length)
(H : s.Nonempty) : (s.sort (· ≤ ·))[(s.sort (· ≤ ·)).length - 1] = s.max' H :=
by
let l := s.sort (· ≤ ·)
apply le_antisymm
· have : l.get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _)
exact s.le_max' _ this
· have : s.max' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.max'_mem H)
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this
rw [← hi]
exact (s.sort_sorted (· ≤ ·)).rel_get_of_le (Nat.le_sub_one_of_lt i.prop)
