s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find (_ : ∃ x, x ∈ s) ≤ m
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m
rw [Nat.sInf_def ⟨m, hm⟩]
no goals
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find (_ : ∃ x, x ∈ s) ≤ m
exact Nat.find_min' ⟨m, hm⟩ hm