Explicitly invoking the well-ordering principle

Stream: mathlib4

[Jeremy Tan]

Surely there's a theorem in mathlib for this, but library_search can't find it

lemma well_ordering_principle (s : Set ℕ) (h : s.Nonempty) : ∃ a ∈ s, ∀ b ∈ s, a ≤ b := by
  sorry

Where is it?

[Jeremy Tan]

This came up in the Carleson project (my code):

lemma antichain_decomposition_exists_k (h : p ∈ 𝔓pos (X := X) ∩ 𝔓₁ᶜ) : ∃ k, p ∈ TilesAt k := by
  let C : Set ℕ := {k | 𝓘 p ∈ aux𝓒 k}
  have Cn : C.Nonempty := by
    rw [mem_inter_iff, 𝔓pos, mem_setOf] at h
    have vpos : 0 < volume (G ∩ 𝓘 p) := by
      rw [inter_comm]; exact h.1.trans_le (measure_mono inter_subset_left)
    obtain ⟨k, hk⟩ := exists_mem_aux𝓒 vpos; exact ⟨_, hk⟩
  -- Then use the well-ordering principle to get `C`'s smallest element `s`. It can't be 0.
  -- So `p ∉ aux𝓒 (s - 1)` and `p ∈ TilesAt s`.
  sorry

[Yaël Dillies]

docs#WellFounded.min

[Jireh Loreaux]

And in particular docs#WellFounded.min_le

[Yury G. Kudryashov]

Also docs#Nat.sInf_mem and docs#csInf_le'

[Yury G. Kudryashov]

Or just docs#isLeast_csInf

[Kevin Buzzard]

Also note docs#Nat.find