refine' ⟨fun h y y_mem ↦ _, fun h ↦ _⟩
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ (x = a ∨ ∀ t ∈ X, x ∈ t) ↔ ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
case h.refine'_1
α : Type u_1
X : Set (Set α)
a x : α
h : x = a ∨ ∀ t ∈ X, x ∈ t
y : Set α
y_mem : y ∈ X
⊢ x = a ∨ x ∈ y

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