α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
x : α
s t : Set α
⊢ s \ {x} ⊆ t ↔ s ⊆ {x} ∪ t
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
x : α
s t : Set α
⊢ s \ {x} ⊆ t ↔ s ⊆ insert x t
rw [← union_singleton, union_comm]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
x : α
s t : Set α
⊢ s \ {x} ⊆ t ↔ s ⊆ {x} ∪ t
apply diff_subset_iff