minimum element exists in any nonempty natural set

Stream: Is there code for X?

[Jihoon Hyun]

import Mathlib.Data.Set.Basic

theorem nonempty_nat_set_contains_minimum {s : Set ℕ} (hs : s.Nonempty) :
    ∃ n ∈ s, ∀ m ∈ s, n ≤ m := by
  by_contra h'
  simp at h'
  rcases hs with ⟨n, hn⟩
  induction n using Nat.strongInductionOn with
  | ind m ihm =>
    rcases h' _ hn with ⟨_, h₁, h₂⟩
    exact ihm _ h₂ h₁

Do we have this theorem in mathlib or std/batteries? If not, which file should this theorem be in?

[Jihoon Hyun]

Plus, is there a definition for the 'minimum element of set of naturals'? I believe this should be noncomputable, though.

[Ruben Van de Velde]

import Mathlib

theorem nonempty_nat_set_contains_minimum {s : Set ℕ} (hs : s.Nonempty) :
    ∃ n ∈ s, ∀ m ∈ s, n ≤ m :=
  ⟨sInf s, Nat.sInf_mem hs, fun m => Nat.sInf_le⟩