intro a s _ _ ih h
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
⊢ ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → (s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t) → insert a s ⊆ ⋃₀ c → ∃ t ∈ c, insert a s ⊆ t
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, insert a s ⊆ t