case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ (∃ a, s = {a}) → Set.Nonempty s ∧ Set.Subsingleton s

case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
h : Set.Nonempty s ∧ Set.Subsingleton s
⊢ ∃ a, s = {a}
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ (∃ a, s = {a}) ↔ Set.Nonempty s ∧ Set.Subsingleton s
refine' ⟨_, fun h => _⟩
case refine'_1.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s₁ s₂ t t₁ t₂ u : Set α
a : α
⊢ Set.Nonempty {a} ∧ Set.Subsingleton {a}
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ (∃ a, s = {a}) → Set.Nonempty s ∧ Set.Subsingleton s
rintro ⟨a, rfl⟩
no goals
case refine'_1.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s₁ s₂ t t₁ t₂ u : Set α
a : α
⊢ Set.Nonempty {a} ∧ Set.Subsingleton {a}
exact ⟨singleton_nonempty a, subsingleton_singleton⟩
no goals
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
h : Set.Nonempty s ∧ Set.Subsingleton s
⊢ ∃ a, s = {a}
exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty