refine ⟨fun h ↦ ?_, fun ⟨t, ht, hst⟩ ↦ subset_sUnion_of_subset _ _ hst ht⟩
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
⊢ s ⊆ ⋃₀ C ↔ ∃ t ∈ C, s ⊆ t
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∃ t ∈ C, s ⊆ t