case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
⊢ ∅ ⊆ {x} ↔ ∅ = ∅ ∨ ∅ = {x}

case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
hs : Set.Nonempty s
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}
obtain rfl | hs := s.eq_empty_or_nonempty
no goals
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
⊢ ∅ ⊆ {x} ↔ ∅ = ∅ ∨ ∅ = {x}
exact ⟨fun _ => Or.inl rfl, fun _ => empty_subset _⟩
no goals
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
hs : Set.Nonempty s
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}
simp [eq_singleton_iff_nonempty_unique_mem, hs, hs.ne_empty]