rcases this with ⟨t, htc, ht⟩
α : 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
this : ∃ t ∈ c, s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t
case intro.intro
α : 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 : Set α
htc : t ∈ c
ht : s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t