no goals
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ ¬m ∈ s
cases eq_empty_or_nonempty s with
| inl h => subst h; apply not_mem_empty
| inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm
case inl
m : ℕ
hm : m < sInf ∅
⊢ ¬m ∈ ∅
case inl
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ ¬m ∈ s
subst h
no goals
case inl
m : ℕ
hm : m < sInf ∅
⊢ ¬m ∈ ∅
apply not_mem_empty
case inr
s : Set ℕ
m : ℕ
h : Set.Nonempty s
hm : m < Nat.find h
⊢ ¬m ∈ s
case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : Set.Nonempty s
⊢ ¬m ∈ s
rw [Nat.sInf_def h] at hm
no goals
case inr
s : Set ℕ
m : ℕ
h : Set.Nonempty s
hm : m < Nat.find h
⊢ ¬m ∈ s
exact Nat.find_min h hm