theorem Set.doubleton_subset {α : Type u_1} {s : Set α} {a b : α} : {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

theorem Set.iff_subset_insert_subset_diff {α : Type u_1} {s t : Set α} {a : α} : s ⊆ insert a t ↔ s \ {a} ⊆ t

theorem Set.ssubset_of_subset_ne {α : Type u_1} {s t : Set α} (h : s ⊆ t) (hne : s ≠ t) : s ⊂ t

theorem Set.infinitely_finset_approximate {α : Type u_1} {s : Set α} {a : α} (count : s.Countable) (inf : s.Infinite) (ha : a ∈ s) : ∃ (f : ℕ → Finset α), f 0 = {a} ∧ (∀ (i : ℕ), f i ⊂ f (i + 1)) ∧ (∀ (i : ℕ), ↑(f i) ⊆ s) ∧ ∀ b ∈ s, ∃ (i : ℕ), b ∈ f i

theorem Set.subset_mem_chain_of_finite {α : Type u_1} (c : Set (Set α)) (hc : c.Nonempty) (hchain : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c) {s : Set α} (hfin : s.Finite) : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t