s : Set ℕ
h : 0 < sInf s
contra : ¬Set.Nonempty s
⊢ False
s : Set ℕ
h : 0 < sInf s
⊢ Set.Nonempty s
by_contra contra
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False
s : Set ℕ
h : 0 < sInf s
contra : ¬Set.Nonempty s
⊢ False
rw [Set.not_nonempty_iff_eq_empty] at contra
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ False
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False
have h' : sInf s ≠ 0 := ne_of_gt h
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ False
apply h'
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ 0 ∈ s ∨ s = ∅
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0
rw [Nat.sInf_eq_zero]
case h
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ 0 ∈ s ∨ s = ∅
right
no goals
case h
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅
assumption