theorem Set.insert_subset_iff
theorem Set.insert_subset_iff: ∀ {α : Type u} {a : α} {s t : Set α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
theorem Set.insert_subset_iff
theorem Set.insert_subset_iff: ∀ {α : Type u} {a : α} {s t : Set α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t