α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ (s ⊆ t ∧ ∃ a, a ∈ t ∧ ¬a ∈ s) ↔ (∃ x x_1, x ∈ t) ∧ s ⊆ t
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ s ⊂ t ↔ ∃ a x, insert a s ⊆ t
simp only [insert_subset, exists_and_right, ssubset_def, not_subset]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ (s ⊆ t ∧ ∃ a, a ∈ t ∧ ¬a ∈ s) ↔ (∃ x x_1, x ∈ t) ∧ s ⊆ t
simp only [exists_prop, and_comm]