no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
P : α → Prop
a : α
s : Set α
⊢ (∃ x, x ∈ insert a s ∧ P x) ↔ P a ∨ ∃ x, x ∈ s ∧ P x
simp [mem_insert_iff, or_and_right, exists_and_left, exists_or]