obtain (rfl | ne) := eq_or_ne x a
case h.refine'_2
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
⊢ x = a ∨ ∀ t ∈ X, x ∈ t
case h.refine'_2.inl
α : Type u_1
X : Set (Set α)
x : α
h : ∀ a ∈ X, x = x ∨ x ∈ a
⊢ x = x ∨ ∀ t ∈ X, x ∈ t

case h.refine'_2.inr
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
ne : x ≠ a
⊢ x = a ∨ ∀ t ∈ X, x ∈ t