no goals
α : Type u_1
β : Type ?u.112523
γ : Type ?u.112526
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
simp only [subset_iff, mem_insert, forall_eq, or_imp, forall_and]