Is this lemma in mathlib?

Stream: mathlib4

[Jeremy Tan]

While working on the Carleson project I had to prove this lemma from scratch, but intuitively it is so simple that it should be in mathlib already. Is it?

import Mathlib.Data.Fintype.Card
import Mathlib.Order.Minimal

variable {α : Type*} [PartialOrder α] [DecidableRel fun x y : α ↦ x ≤ y] (s : Finset α)

lemma exists_ge_in_maximals : ∀ i ∈ s, ∃ j ∈ maximals (· ≤ ·) s, i ≤ j := fun i hi ↦ by
  let C : Finset α := s.filter (i ≤ ·)
  have Cn : C.Nonempty := ⟨i, by simp only [C, Finset.mem_filter, hi, le_rfl, true_and]⟩
  obtain ⟨j, hj, maxj⟩ := C.exists_maximal Cn
  simp_rw [C, Finset.mem_filter] at hj maxj ⊢
  refine ⟨j, ?_, hj.2⟩
  rw [mem_maximals_iff]
  refine ⟨hj.1, fun k hk lk ↦ eq_of_le_of_not_lt lk (maxj k ⟨hk, hj.2.trans lk⟩)⟩

[Yaël Dillies]

Try to find this statement as s \subset lowerClosure (minimals s)

[Jeremy Tan]

Well, it doesn't exist

[Peter Nelson]

You can apply Finite.exists_maximal_wrt to the identity function and the Finite set of elements of s above i.

[Peter Nelson]

... I suppose this is no better than the proof you have above.

On this topic: maximals being a set rather than a predicate has always seemed wrong to me. It seems like a good candidate for dot notation, with lemmas like Maximal.eq_of_le, Maximal.not_lt, and specializations to Set/Finset like Maximal.not_ssubset etc.

This would also reflect informal usage better. Maximality really is a property rather than a collection: we say 'x is maximal with property P', not 'x belongs to the set of maximal elements with property P'.

[Yaël Dillies]

Yeah sure. I quickly put maximals together three years ago and I didn't spend that much time thinking about whether it should be a set or a predicate