no goals
s : Set ℕ
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
cases eq_empty_or_nonempty s with
| inl h => subst h
           simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf,
                      mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
| inr h => simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
case inl

⊢ sInf ∅ = 0 ↔ 0 ∈ ∅ ∨ ∅ = ∅
case inl
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
subst h
no goals
case inl

⊢ sInf ∅ = 0 ↔ 0 ∈ ∅ ∨ ∅ = ∅
simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf,
           mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
no goals
case inr
s : Set ℕ
h : Set.Nonempty s
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]